The dog is red. The mouse sees the squirrel. The rabbit chases the dog. The rabbit is cold. The squirrel chases the dog. The squirrel chases the mouse. The squirrel chases the rabbit. The squirrel eats the mouse. The squirrel eats the rabbit. The squirrel is blue. If something chases the dog then it is cold. If something is rough then it chases the mouse. If something eats the squirrel then the squirrel eats the dog. If something chases the rabbit then the rabbit is blue. If something eats the mouse and it chases the rabbit then the mouse eats the dog. If something is cold and it chases the mouse then it eats the squirrel. If something eats the dog and it is nice then it eats the rabbit. If something chases the mouse then it is cold.
The dog is red.
("dog" "is" "red" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
If something chases the dog then it is cold.
((("something" "chases" "dog" "+")) -> ("something" "is" "cold" "+"))
If something is rough then it chases the mouse.
((("something" "is" "rough" "+")) -> ("something" "chases" "mouse" "+"))
If something eats the squirrel then the squirrel eats the dog.
((("something" "eats" "squirrel" "+")) -> ("squirrel" "eats" "dog" "+"))
If something chases the rabbit then the rabbit is blue.
((("something" "chases" "rabbit" "+")) -> ("rabbit" "is" "blue" "+"))
If something eats the mouse and it chases the rabbit then the mouse eats the dog.
((("something" "eats" "mouse" "+") ("something" "chases" "rabbit" "+")) -> ("mouse" "eats" "dog" "+"))
If something is cold and it chases the mouse then it eats the squirrel.
((("something" "is" "cold" "+") ("something" "chases" "mouse" "+")) -> ("something" "eats" "squirrel" "+"))
If something eats the dog and it is nice then it eats the rabbit.
((("something" "eats" "dog" "+") ("something" "is" "nice" "+")) -> ("something" "eats" "rabbit" "+"))
If something chases the mouse then it is cold.
((("something" "chases" "mouse" "+")) -> ("something" "is" "cold" "+"))
The mouse sees the squirrel.
True
1
proof
[(triple2)]
("mouse" "sees" "squirrel" "+")
triple2
The squirrel does not chase the rabbit.
False
1
inv-proof
[(triple7)]
("squirrel" "chases" "rabbit" "-")
triple7
The mouse eats the dog.
True
3
proof
[(((triple8 triple7) -> rule5))]
("mouse" "eats" "dog" "+")
((triple8 triple7) -> (rule5 % int1))
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int1
The mouse does not eat the dog.
False
3
inv-proof
[(((triple8 triple7) -> rule5))]
("mouse" "eats" "dog" "-")
((triple8 triple7) -> (rule5 % int1))
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int1
The squirrel eats the squirrel.
True
4
proof
[(((((triple5) -> rule1) triple6) -> rule6) OR ((((triple6) -> rule8) triple6) -> rule6))]
("squirrel" "eats" "squirrel" "+")
((((triple5) -> (rule1 % int2)) triple6) -> (rule6 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
((((triple6) -> (rule8 % int2)) triple6) -> (rule6 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The squirrel does not eat the squirrel.
False
4
inv-proof
[(((((triple5) -> rule1) triple6) -> rule6) OR ((((triple6) -> rule8) triple6) -> rule6))]
("squirrel" "eats" "squirrel" "-")
((((triple5) -> (rule1 % int2)) triple6) -> (rule6 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
((((triple6) -> (rule8 % int2)) triple6) -> (rule6 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The squirrel eats the dog.
True
5
proof
[(((((((triple5) -> rule1) triple6) -> rule6)) -> rule3) OR ((((((triple6) -> rule8) triple6) -> rule6)) -> rule3))]
("squirrel" "eats" "dog" "+")
((((((triple5) -> (rule1 % int3)) triple6) -> (rule6 % int2))) -> (rule3 % int1))
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
((((((triple6) -> (rule8 % int3)) triple6) -> (rule6 % int2))) -> (rule3 % int1))
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
The squirrel does not eat the dog.
False
5
inv-proof
[(((((((triple5) -> rule1) triple6) -> rule6)) -> rule3) OR ((((((triple6) -> rule8) triple6) -> rule6)) -> rule3))]
("squirrel" "eats" "dog" "-")
((((((triple5) -> (rule1 % int3)) triple6) -> (rule6 % int2))) -> (rule3 % int1))
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
((((((triple6) -> (rule8 % int3)) triple6) -> (rule6 % int2))) -> (rule3 % int1))
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
The mouse does not eat the rabbit.
Unknown
inv-rconc
[@1: The mouse eats the rabbit.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "eats" "rabbit" "-")
The mouse is cold.
Unknown
rconc
[@2: The mouse is cold.[CWA. Example of deepest failure = (rule8 <- rule2 <- FAIL)]]
("mouse" "is" "cold" "+")
The rabbit does not chase the mouse.
Unknown
inv-rconc
[@1: The rabbit chases the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "chases" "mouse" "-")
The rabbit eats the squirrel.
Unknown
rconc
[@2: The rabbit eats the squirrel.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("rabbit" "eats" "squirrel" "+")
The squirrel is not red.
Unknown
inv-random
[@0: The squirrel is red.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "red" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
The squirrel is not nice.
Unknown
inv-random
[@0: The squirrel is nice.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "nice" "-")
The rabbit chases the squirrel.
Unknown
random
[@0: The rabbit chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "squirrel" "+")
@0: The dog is red.[(triple1)] The mouse sees the squirrel.[(triple2)] The rabbit chases the dog.[(triple3)] The rabbit is cold.[(triple4 OR ((triple3) -> rule1))] The squirrel chases the dog.[(triple5)] The squirrel chases the mouse.[(triple6)] The squirrel chases the rabbit.[(triple7)] The squirrel eats the mouse.[(triple8)] The squirrel eats the rabbit.[(triple9)] The squirrel is blue.[(triple10)] @1: The mouse eats the dog.[(((triple8 triple7) -> rule5))] The rabbit is blue.[(((triple7) -> rule4))] The squirrel is cold.[(((triple5) -> rule1) OR ((triple6) -> rule8))] @2: The squirrel eats the squirrel.[(((((triple5) -> rule1) triple6) -> rule6) OR ((((triple6) -> rule8) triple6) -> rule6))] @3: The squirrel eats the dog.[(((((((triple5) -> rule1) triple6) -> rule6)) -> rule3) OR ((((((triple6) -> rule8) triple6) -> rule6)) -> rule3))]
The dog is red.
("dog" "is" "red" "+")
triple1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple2
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
triple3
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple4
((triple3) -> (rule1 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
triple5
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
triple6
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
triple7
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple8
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
triple9
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple10
The mouse eats the dog.
("mouse" "eats" "dog" "+")
((triple8 triple7) -> (rule5 % int1))
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
((triple7) -> (rule4 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
((triple5) -> (rule1 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
((triple6) -> (rule8 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
((((triple5) -> (rule1 % int2)) triple6) -> (rule6 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
((((triple6) -> (rule8 % int2)) triple6) -> (rule6 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
((((((triple5) -> (rule1 % int3)) triple6) -> (rule6 % int2))) -> (rule3 % int1))
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
((((((triple6) -> (rule8 % int3)) triple6) -> (rule6 % int2))) -> (rule3 % int1))
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3