The cat eats the dog. The cat eats the mouse. The cat is kind. The cat is round. The dog does not see the cat. The mouse is kind. The mouse needs the rabbit. The rabbit eats the cat. The rabbit is not cold. The rabbit needs the mouse. The rabbit sees the cat. If someone sees the mouse then the mouse is rough. If someone is red then they are rough. If someone eats the dog and they do not need the dog then they need the cat. If someone needs the mouse and they see the cat then the cat is red. If someone is round then they see the cat. If someone is rough then they see the mouse. If the cat eats the mouse and the cat does not see the dog then the dog is red. If someone is red and not rough then they do not eat the cat.
The cat eats the dog.
("cat" "eats" "dog" "+")
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is round.
("cat" "is" "round" "+")
The dog does not see the cat.
("dog" "sees" "cat" "-")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
The rabbit is not cold.
("rabbit" "is" "cold" "-")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
If someone sees the mouse then the mouse is rough.
((("someone" "sees" "mouse" "+")) -> ("mouse" "is" "rough" "+"))
If someone is red then they are rough.
((("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
If someone eats the dog and they do not need the dog then they need the cat.
((("someone" "eats" "dog" "+") ("someone" "needs" "dog" "~")) -> ("someone" "needs" "cat" "+"))
If someone needs the mouse and they see the cat then the cat is red.
((("someone" "needs" "mouse" "+") ("someone" "sees" "cat" "+")) -> ("cat" "is" "red" "+"))
If someone is round then they see the cat.
((("someone" "is" "round" "+")) -> ("someone" "sees" "cat" "+"))
If someone is rough then they see the mouse.
((("someone" "is" "rough" "+")) -> ("someone" "sees" "mouse" "+"))
If the cat eats the mouse and the cat does not see the dog then the dog is red.
((("cat" "eats" "mouse" "+") ("cat" "sees" "dog" "~")) -> ("dog" "is" "red" "+"))
If someone is red and not rough then they do not eat the cat.
((("someone" "is" "red" "+") ("someone" "is" "rough" "~")) -> ("someone" "eats" "cat" "-"))
The rabbit is not cold.
True
1
proof
[(triple9)]
("rabbit" "is" "cold" "-")
triple9
The rabbit is cold.
False
1
inv-proof
[(triple9)]
("rabbit" "is" "cold" "+")
triple9
The cat is red.
True
3
proof
[(((triple10 triple11) -> rule4))]
("cat" "is" "red" "+")
((triple10 triple11) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat does not see the cat.
False
2
inv-proof
[(((triple4) -> rule5))]
("cat" "sees" "cat" "-")
((triple4) -> (rule5 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat is rough.
True
4
proof
[(((((triple10 triple11) -> rule4)) -> rule2))]
("cat" "is" "rough" "+")
((((triple10 triple11) -> (rule4 % int2))) -> (rule2 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is not rough.
False
4
inv-proof
[(((((triple10 triple11) -> rule4)) -> rule2))]
("cat" "is" "rough" "-")
((((triple10 triple11) -> (rule4 % int2))) -> (rule2 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat sees the mouse.
True
5
proof
[(((((((triple10 triple11) -> rule4)) -> rule2)) -> rule6))]
("cat" "sees" "mouse" "+")
((((((triple10 triple11) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The cat does not see the mouse.
False
5
inv-proof
[(((((((triple10 triple11) -> rule4)) -> rule2)) -> rule6))]
("cat" "sees" "mouse" "-")
((((((triple10 triple11) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The mouse is rough.
True
6
proof
[(((((((((triple10 triple11) -> rule4)) -> rule2)) -> rule6)) -> rule1))]
("mouse" "is" "rough" "+")
((((((((triple10 triple11) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
The cat is red.
("cat" "is" "red" "+")
int4
The mouse is not rough.
False
6
inv-proof
[(((((((((triple10 triple11) -> rule4)) -> rule2)) -> rule6)) -> rule1))]
("mouse" "is" "rough" "-")
((((((((triple10 triple11) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
The cat is red.
("cat" "is" "red" "+")
int4
The mouse sees the mouse.
True
7
proof
[(((((((((((triple10 triple11) -> rule4)) -> rule2)) -> rule6)) -> rule1)) -> rule6))]
("mouse" "sees" "mouse" "+")
((((((((((triple10 triple11) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int3
The cat is rough.
("cat" "is" "rough" "+")
int4
The cat is red.
("cat" "is" "red" "+")
int5
The mouse does not see the mouse.
False
7
inv-proof
[(((((((((((triple10 triple11) -> rule4)) -> rule2)) -> rule6)) -> rule1)) -> rule6))]
("mouse" "sees" "mouse" "-")
((((((((((triple10 triple11) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int3
The cat is rough.
("cat" "is" "rough" "+")
int4
The cat is red.
("cat" "is" "red" "+")
int5
The rabbit does not see the mouse.
Unknown
inv-rconc
[@2: The rabbit sees the mouse.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("rabbit" "sees" "mouse" "-")
The rabbit needs the cat.
Unknown
rconc
[@1: The rabbit needs the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "needs" "cat" "+")
The dog does not need the cat.
Unknown
inv-rconc
[@1: The dog needs the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "needs" "cat" "-")
The dog sees the mouse.
Unknown
rconc
[@3: The dog sees the mouse.[CWA. Example of deepest failure = (rule6 <- rule2 <- rule7 <- FAIL)]]
("dog" "sees" "mouse" "+")
The rabbit is not rough.
Unknown
inv-rconc
[@1: The rabbit is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "rough" "-")
The mouse needs the cat.
Unknown
rconc
[@1: The mouse needs the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "needs" "cat" "+")
The dog is not cold.
Unknown
inv-random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "-")
The cat needs the dog.
Unknown
random
[@0: The cat needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "dog" "+")
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
The mouse is red.
Unknown
random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "+")
The cat is not cold.
Unknown
inv-random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "-")
The cat eats the rabbit.
Unknown
random
[@0: The cat eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "rabbit" "+")
@0: The cat eats the dog.[(triple1)] The cat eats the mouse.[(triple2)] The cat is kind.[(triple3)] The cat is round.[(triple4)] The dog does not see the cat.[(triple5)] The mouse is kind.[(triple6)] The mouse needs the rabbit.[(triple7)] The rabbit eats the cat.[(triple8)] The rabbit is not cold.[(triple9)] The rabbit needs the mouse.[(triple10)] The rabbit sees the cat.[(triple11)] @1: The cat is red.[(((triple10 triple11) -> rule4))] The cat sees the cat.[(((triple4) -> rule5))] @2: The cat is rough.[(((((triple10 triple11) -> rule4)) -> rule2))] @3: The cat sees the mouse.[(((((((triple10 triple11) -> rule4)) -> rule2)) -> rule6))] @4: The mouse is rough.[(((((((((triple10 triple11) -> rule4)) -> rule2)) -> rule6)) -> rule1))] @5: The mouse sees the mouse.[(((((((((((triple10 triple11) -> rule4)) -> rule2)) -> rule6)) -> rule1)) -> rule6))]
The cat eats the dog.
("cat" "eats" "dog" "+")
triple1
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple2
The cat is kind.
("cat" "is" "kind" "+")
triple3
The cat is round.
("cat" "is" "round" "+")
triple4
The dog does not see the cat.
("dog" "sees" "cat" "-")
triple5
The mouse is kind.
("mouse" "is" "kind" "+")
triple6
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple7
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
triple8
The rabbit is not cold.
("rabbit" "is" "cold" "-")
triple9
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple10
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple11
The cat is red.
("cat" "is" "red" "+")
((triple10 triple11) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
((triple4) -> (rule5 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
((((triple10 triple11) -> (rule4 % int2))) -> (rule2 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat sees the mouse.
("cat" "sees" "mouse" "+")
((((((triple10 triple11) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The mouse is rough.
("mouse" "is" "rough" "+")
((((((((triple10 triple11) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
The cat is red.
("cat" "is" "red" "+")
int4
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((((((((((triple10 triple11) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int3
The cat is rough.
("cat" "is" "rough" "+")
int4
The cat is red.
("cat" "is" "red" "+")
int5