The cat chases the mouse. The cat is nice. The cat does not like the dog. The cat likes the tiger. The dog is not kind. The dog likes the cat. The mouse is blue. The tiger chases the cat. The tiger chases the dog. The tiger is blue. The tiger likes the cat. The tiger does not see the cat. If something is kind then it likes the cat. If something sees the dog then the dog does not see the cat. If the tiger is nice then the tiger does not see the cat. If something is round then it does not chase the dog. If something is cold then it does not chase the mouse. If something likes the tiger then it sees the mouse. If something is blue then it is cold. If the dog does not chase the mouse and the dog does not see the mouse then the mouse does not chase the dog.
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat does not like the dog.
("cat" "likes" "dog" "-")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The dog is not kind.
("dog" "is" "kind" "-")
The dog likes the cat.
("dog" "likes" "cat" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
The tiger chases the dog.
("tiger" "chases" "dog" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
The tiger does not see the cat.
("tiger" "sees" "cat" "-")
If something is kind then it likes the cat.
((("something" "is" "kind" "+")) -> ("something" "likes" "cat" "+"))
If something sees the dog then the dog does not see the cat.
((("something" "sees" "dog" "+")) -> ("dog" "sees" "cat" "-"))
If the tiger is nice then the tiger does not see the cat.
((("tiger" "is" "nice" "+")) -> ("tiger" "sees" "cat" "-"))
If something is round then it does not chase the dog.
((("something" "is" "round" "+")) -> ("something" "chases" "dog" "-"))
If something is cold then it does not chase the mouse.
((("something" "is" "cold" "+")) -> ("something" "chases" "mouse" "-"))
If something likes the tiger then it sees the mouse.
((("something" "likes" "tiger" "+")) -> ("something" "sees" "mouse" "+"))
If something is blue then it is cold.
((("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
If the dog does not chase the mouse and the dog does not see the mouse then the mouse does not chase the dog.
((("dog" "chases" "mouse" "~") ("dog" "sees" "mouse" "~")) -> ("mouse" "chases" "dog" "-"))
The dog is not kind.
True
1
proof
[(triple5)]
("dog" "is" "kind" "-")
triple5
The cat is not nice.
False
1
inv-proof
[(triple2)]
("cat" "is" "nice" "-")
triple2
The tiger is cold.
True
2
proof
[(((triple10) -> rule7))]
("tiger" "is" "cold" "+")
((triple10) -> (rule7 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The mouse is not cold.
False
2
inv-proof
[(((triple7) -> rule7))]
("mouse" "is" "cold" "-")
((triple7) -> (rule7 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse does not chase the mouse.
True
3
proof
[(((((triple7) -> rule7)) -> rule5))]
("mouse" "chases" "mouse" "-")
((((triple7) -> (rule7 % int2))) -> (rule5 % int1))
The mouse does not chase the mouse.
("mouse" "chases" "mouse" "-")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse chases the mouse.
False
3
inv-proof
[(((((triple7) -> rule7)) -> rule5))]
("mouse" "chases" "mouse" "+")
((((triple7) -> (rule7 % int2))) -> (rule5 % int1))
The mouse does not chase the mouse.
("mouse" "chases" "mouse" "-")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The cat does not like the cat.
Unknown
inv-rconc
[@1: The cat likes the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "likes" "cat" "-")
The cat is cold.
Unknown
rconc
[@1: The cat is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "is" "cold" "+")
The dog is not cold.
Unknown
inv-rconc
[@1: The dog is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "is" "cold" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
The mouse does not see the dog.
Unknown
inv-random
[@0: The mouse sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "dog" "-")
The dog is nice.
Unknown
random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "+")
@0: The cat chases the mouse.[(triple1)] The cat does not like the dog.[(triple3)] The cat is nice.[(triple2)] The cat likes the tiger.[(triple4)] The dog is not kind.[(triple5)] The dog likes the cat.[(triple6)] The mouse is blue.[(triple7)] The tiger chases the cat.[(triple8)] The tiger chases the dog.[(triple9)] The tiger does not see the cat.[(triple12)] The tiger is blue.[(triple10)] The tiger likes the cat.[(triple11)] @1: The cat sees the mouse.[(((triple4) -> rule6))] The mouse is cold.[(((triple7) -> rule7))] The tiger is cold.[(((triple10) -> rule7))] @2: The mouse does not chase the mouse.[(((((triple7) -> rule7)) -> rule5))] The tiger does not chase the mouse.[(((((triple10) -> rule7)) -> rule5))]
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple1
The cat does not like the dog.
("cat" "likes" "dog" "-")
triple3
The cat is nice.
("cat" "is" "nice" "+")
triple2
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple4
The dog is not kind.
("dog" "is" "kind" "-")
triple5
The dog likes the cat.
("dog" "likes" "cat" "+")
triple6
The mouse is blue.
("mouse" "is" "blue" "+")
triple7
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple8
The tiger chases the dog.
("tiger" "chases" "dog" "+")
triple9
The tiger does not see the cat.
("tiger" "sees" "cat" "-")
triple12
The tiger is blue.
("tiger" "is" "blue" "+")
triple10
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple11
The cat sees the mouse.
("cat" "sees" "mouse" "+")
((triple4) -> (rule6 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
((triple7) -> (rule7 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
((triple10) -> (rule7 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The mouse does not chase the mouse.
("mouse" "chases" "mouse" "-")
((((triple7) -> (rule7 % int2))) -> (rule5 % int1))
The mouse does not chase the mouse.
("mouse" "chases" "mouse" "-")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The tiger does not chase the mouse.
("tiger" "chases" "mouse" "-")
((((triple10) -> (rule7 % int2))) -> (rule5 % int1))
The tiger does not chase the mouse.
("tiger" "chases" "mouse" "-")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2