The cat does not chase the rabbit. The cat is blue. The cat is red. The cat visits the tiger. The mouse is green. The mouse likes the rabbit. The rabbit is blue. The tiger is green. The tiger is rough. The tiger likes the rabbit. Blue people are red. If someone is red then they chase the mouse. If someone likes the mouse and the mouse chases the cat then the mouse does not like the tiger. If someone is rough then they like the tiger. If someone is green then they are blue. If someone likes the cat and they do not like the mouse then the cat does not chase the rabbit.
The cat does not chase the rabbit.
("cat" "chases" "rabbit" "-")
The cat is blue.
("cat" "is" "blue" "+")
The cat is red.
("cat" "is" "red" "+")
The cat visits the tiger.
("cat" "visits" "tiger" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
Blue people are red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
If someone is red then they chase the mouse.
((("someone" "is" "red" "+")) -> ("someone" "chases" "mouse" "+"))
If someone likes the mouse and the mouse chases the cat then the mouse does not like the tiger.
((("someone" "likes" "mouse" "+") ("mouse" "chases" "cat" "+")) -> ("mouse" "likes" "tiger" "-"))
If someone is rough then they like the tiger.
((("someone" "is" "rough" "+")) -> ("someone" "likes" "tiger" "+"))
If someone is green then they are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
If someone likes the cat and they do not like the mouse then the cat does not chase the rabbit.
((("someone" "likes" "cat" "+") ("someone" "likes" "mouse" "~")) -> ("cat" "chases" "rabbit" "-"))
The tiger is rough.
True
1
proof
[(triple9)]
("tiger" "is" "rough" "+")
triple9
The cat does not visit the tiger.
False
1
inv-proof
[(triple4)]
("cat" "visits" "tiger" "-")
triple4
The tiger likes the tiger.
True
2
proof
[(((triple9) -> rule4))]
("tiger" "likes" "tiger" "+")
((triple9) -> (rule4 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger does not like the tiger.
False
2
inv-proof
[(((triple9) -> rule4))]
("tiger" "likes" "tiger" "-")
((triple9) -> (rule4 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The rabbit chases the mouse.
True
3
proof
[(((((triple7) -> rule1)) -> rule2))]
("rabbit" "chases" "mouse" "+")
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The tiger is not red.
False
3
inv-proof
[(((((triple8) -> rule5)) -> rule1))]
("tiger" "is" "red" "-")
((((triple8) -> (rule5 % int2))) -> (rule1 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger chases the mouse.
True
4
proof
[(((((((triple8) -> rule5)) -> rule1)) -> rule2))]
("tiger" "chases" "mouse" "+")
((((((triple8) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
int3
The tiger does not chase the mouse.
False
4
inv-proof
[(((((((triple8) -> rule5)) -> rule1)) -> rule2))]
("tiger" "chases" "mouse" "-")
((((((triple8) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
int3
The rabbit does not like the tiger.
Unknown
inv-rconc
[@1: The rabbit likes the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "likes" "tiger" "-")
The cat likes the tiger.
Unknown
rconc
[@1: The cat likes the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "likes" "tiger" "+")
The mouse does not like the tiger.
Unknown
inv-rconc
[@1: The mouse likes the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "likes" "tiger" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
The rabbit is not rough.
Unknown
inv-random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
The rabbit does not visit the mouse.
Unknown
inv-random
[@0: The rabbit visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "mouse" "-")
The mouse is rough.
Unknown
random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "+")
@0: The cat does not chase the rabbit.[(triple1)] The cat is blue.[(triple2)] The cat is red.[(triple3 OR ((triple2) -> rule1))] The cat visits the tiger.[(triple4)] The mouse is green.[(triple5)] The mouse likes the rabbit.[(triple6)] The rabbit is blue.[(triple7)] The tiger is green.[(triple8)] The tiger is rough.[(triple9)] The tiger likes the rabbit.[(triple10)] @1: The cat chases the mouse.[(((triple3) -> rule2) OR ((((triple2) -> rule1)) -> rule2))] The mouse is blue.[(((triple5) -> rule5))] The rabbit is red.[(((triple7) -> rule1))] The tiger is blue.[(((triple8) -> rule5))] The tiger likes the tiger.[(((triple9) -> rule4))] @2: The mouse is red.[(((((triple5) -> rule5)) -> rule1))] The rabbit chases the mouse.[(((((triple7) -> rule1)) -> rule2))] The tiger is red.[(((((triple8) -> rule5)) -> rule1))] @3: The mouse chases the mouse.[(((((((triple5) -> rule5)) -> rule1)) -> rule2))] The tiger chases the mouse.[(((((((triple8) -> rule5)) -> rule1)) -> rule2))]
The cat does not chase the rabbit.
("cat" "chases" "rabbit" "-")
triple1
The cat is blue.
("cat" "is" "blue" "+")
triple2
The cat is red.
("cat" "is" "red" "+")
triple3
((triple2) -> (rule1 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat visits the tiger.
("cat" "visits" "tiger" "+")
triple4
The mouse is green.
("mouse" "is" "green" "+")
triple5
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
triple6
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple7
The tiger is green.
("tiger" "is" "green" "+")
triple8
The tiger is rough.
("tiger" "is" "rough" "+")
triple9
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple10
The cat chases the mouse.
("cat" "chases" "mouse" "+")
((triple3) -> (rule2 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
((triple5) -> (rule5 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
((triple7) -> (rule1 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
((triple8) -> (rule5 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((triple9) -> (rule4 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
((((triple5) -> (rule5 % int2))) -> (rule1 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
((((triple8) -> (rule5 % int2))) -> (rule1 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((((((triple5) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
((((((triple8) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
int3