The cat is cold. The cat likes the mouse. The cat likes the rabbit. The cat does not see the rabbit. The cat does not visit the mouse. The mouse is kind. The mouse is red. The mouse likes the cat. The mouse does not see the rabbit. The mouse visits the rabbit. The rabbit sees the cat. The rabbit visits the mouse. If the rabbit is round and the rabbit does not visit the cat then the rabbit is not green. If something is red and it likes the rabbit then it is green. Cold things are red. If the mouse visits the rabbit then the mouse visits the cat. If something visits the rabbit then it is cold. If something visits the cat then it likes the rabbit.
The cat is cold.
("cat" "is" "cold" "+")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The cat does not see the rabbit.
("cat" "sees" "rabbit" "-")
The cat does not visit the mouse.
("cat" "visits" "mouse" "-")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The mouse does not see the rabbit.
("mouse" "sees" "rabbit" "-")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
If the rabbit is round and the rabbit does not visit the cat then the rabbit is not green.
((("rabbit" "is" "round" "+") ("rabbit" "visits" "cat" "~")) -> ("rabbit" "is" "green" "-"))
If something is red and it likes the rabbit then it is green.
((("something" "is" "red" "+") ("something" "likes" "rabbit" "+")) -> ("something" "is" "green" "+"))
Cold things are red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
If the mouse visits the rabbit then the mouse visits the cat.
((("mouse" "visits" "rabbit" "+")) -> ("mouse" "visits" "cat" "+"))
If something visits the rabbit then it is cold.
((("something" "visits" "rabbit" "+")) -> ("something" "is" "cold" "+"))
If something visits the cat then it likes the rabbit.
((("something" "visits" "cat" "+")) -> ("something" "likes" "rabbit" "+"))
The mouse likes the cat.
True
1
proof
[(triple8)]
("mouse" "likes" "cat" "+")
triple8
The mouse does not visit the rabbit.
False
1
inv-proof
[(triple10)]
("mouse" "visits" "rabbit" "-")
triple10
The mouse visits the cat.
True
2
proof
[(((triple10) -> rule4))]
("mouse" "visits" "cat" "+")
((triple10) -> (rule4 % int1))
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int1
The mouse is not cold.
False
2
inv-proof
[(((triple10) -> rule5))]
("mouse" "is" "cold" "-")
((triple10) -> (rule5 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse likes the rabbit.
True
3
proof
[(((((triple10) -> rule4)) -> rule6))]
("mouse" "likes" "rabbit" "+")
((((triple10) -> (rule4 % int2))) -> (rule6 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int2
The mouse does not like the rabbit.
False
3
inv-proof
[(((((triple10) -> rule4)) -> rule6))]
("mouse" "likes" "rabbit" "-")
((((triple10) -> (rule4 % int2))) -> (rule6 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int2
The mouse is green.
True
5
proof
[(((triple7 ((((triple10) -> rule4)) -> rule6)) -> rule2) OR ((((((triple10) -> rule5)) -> rule3) ((((triple10) -> rule4)) -> rule6)) -> rule2))]
("mouse" "is" "green" "+")
((triple7 ((((triple10) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int3
((((((triple10) -> (rule5 % int5))) -> (rule3 % int4)) ((((triple10) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int3
The mouse is red.
("mouse" "is" "red" "+")
int4
The mouse is cold.
("mouse" "is" "cold" "+")
int5
The mouse is not green.
False
5
inv-proof
[(((triple7 ((((triple10) -> rule4)) -> rule6)) -> rule2) OR ((((((triple10) -> rule5)) -> rule3) ((((triple10) -> rule4)) -> rule6)) -> rule2))]
("mouse" "is" "green" "-")
((triple7 ((((triple10) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int3
((((((triple10) -> (rule5 % int5))) -> (rule3 % int4)) ((((triple10) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int3
The mouse is red.
("mouse" "is" "red" "+")
int4
The mouse is cold.
("mouse" "is" "cold" "+")
int5
The rabbit is not red.
Unknown
inv-rconc
[@2: The rabbit is red.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("rabbit" "is" "red" "-")
The rabbit is green.
Unknown
rconc
[@2: The rabbit is green.[CWA. Example of deepest failure = (rule2 <- rule6 <- FAIL)]]
("rabbit" "is" "green" "+")
The rabbit does not like the rabbit.
Unknown
inv-rconc
[@1: The rabbit likes the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "likes" "rabbit" "-")
The rabbit is cold.
Unknown
rconc
[@1: The rabbit is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "is" "cold" "+")
The mouse is not round.
Unknown
inv-random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "-")
The cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
The rabbit does not like the cat.
Unknown
inv-random
[@0: The rabbit likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "cat" "-")
The rabbit visits the cat.
Unknown
random
[@0: The rabbit visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "cat" "+")
@0: The cat does not see the rabbit.[(triple4)] The cat does not visit the mouse.[(triple5)] The cat is cold.[(triple1)] The cat likes the mouse.[(triple2)] The cat likes the rabbit.[(triple3)] The mouse does not see the rabbit.[(triple9)] The mouse is kind.[(triple6)] The mouse is red.[(triple7 OR ((((triple10) -> rule5)) -> rule3))] The mouse likes the cat.[(triple8)] The mouse visits the rabbit.[(triple10)] The rabbit sees the cat.[(triple11)] The rabbit visits the mouse.[(triple12)] @1: The cat is red.[(((triple1) -> rule3))] The mouse is cold.[(((triple10) -> rule5))] The mouse visits the cat.[(((triple10) -> rule4))] @2: The cat is green.[(((((triple1) -> rule3) triple3) -> rule2))] The mouse likes the rabbit.[(((((triple10) -> rule4)) -> rule6))] @3: The mouse is green.[(((triple7 ((((triple10) -> rule4)) -> rule6)) -> rule2) OR ((((((triple10) -> rule5)) -> rule3) ((((triple10) -> rule4)) -> rule6)) -> rule2))]
The cat does not see the rabbit.
("cat" "sees" "rabbit" "-")
triple4
The cat does not visit the mouse.
("cat" "visits" "mouse" "-")
triple5
The cat is cold.
("cat" "is" "cold" "+")
triple1
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple2
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple3
The mouse does not see the rabbit.
("mouse" "sees" "rabbit" "-")
triple9
The mouse is kind.
("mouse" "is" "kind" "+")
triple6
The mouse is red.
("mouse" "is" "red" "+")
triple7
((((triple10) -> (rule5 % int2))) -> (rule3 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple8
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple10
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple11
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple12
The cat is red.
("cat" "is" "red" "+")
((triple1) -> (rule3 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
((triple10) -> (rule5 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse visits the cat.
("mouse" "visits" "cat" "+")
((triple10) -> (rule4 % int1))
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int1
The cat is green.
("cat" "is" "green" "+")
((((triple1) -> (rule3 % int2)) triple3) -> (rule2 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
((((triple10) -> (rule4 % int2))) -> (rule6 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
((triple7 ((((triple10) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int3
((((((triple10) -> (rule5 % int5))) -> (rule3 % int4)) ((((triple10) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int3
The mouse is red.
("mouse" "is" "red" "+")
int4
The mouse is cold.
("mouse" "is" "cold" "+")
int5