The cat eats the tiger. The cat is blue. The mouse is cold. The mouse is rough. The mouse visits the tiger. The squirrel is cold. The squirrel sees the tiger. The tiger eats the mouse. The tiger eats the squirrel. The tiger is rough. The tiger visits the cat. If something is rough then it sees the squirrel. If something visits the tiger then it is young. If something is cold and it sees the squirrel then it is rough. If something eats the squirrel then it eats the tiger. If something is cold and rough then it visits the tiger. If something is young then it sees the mouse. If something is cold then it sees the squirrel.
The cat eats the tiger.
("cat" "eats" "tiger" "+")
The cat is blue.
("cat" "is" "blue" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If something is rough then it sees the squirrel.
((("something" "is" "rough" "+")) -> ("something" "sees" "squirrel" "+"))
If something visits the tiger then it is young.
((("something" "visits" "tiger" "+")) -> ("something" "is" "young" "+"))
If something is cold and it sees the squirrel then it is rough.
((("something" "is" "cold" "+") ("something" "sees" "squirrel" "+")) -> ("something" "is" "rough" "+"))
If something eats the squirrel then it eats the tiger.
((("something" "eats" "squirrel" "+")) -> ("something" "eats" "tiger" "+"))
If something is cold and rough then it visits the tiger.
((("something" "is" "cold" "+") ("something" "is" "rough" "+")) -> ("something" "visits" "tiger" "+"))
If something is young then it sees the mouse.
((("something" "is" "young" "+")) -> ("something" "sees" "mouse" "+"))
If something is cold then it sees the squirrel.
((("something" "is" "cold" "+")) -> ("something" "sees" "squirrel" "+"))
The tiger eats the squirrel.
True
1
proof
[(triple9)]
("tiger" "eats" "squirrel" "+")
triple9
The tiger is not rough.
False
1
inv-proof
[(triple10)]
("tiger" "is" "rough" "-")
triple10
The tiger eats the tiger.
True
2
proof
[(((triple9) -> rule4))]
("tiger" "eats" "tiger" "+")
((triple9) -> (rule4 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The squirrel does not see the squirrel.
False
2
inv-proof
[(((triple6) -> rule7))]
("squirrel" "sees" "squirrel" "-")
((triple6) -> (rule7 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel is rough.
True
4
proof
[(((triple6 ((triple6) -> rule7)) -> rule3))]
("squirrel" "is" "rough" "+")
((triple6 ((triple6) -> (rule7 % int2))) -> (rule3 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
The squirrel is not rough.
False
4
inv-proof
[(((triple6 ((triple6) -> rule7)) -> rule3))]
("squirrel" "is" "rough" "-")
((triple6 ((triple6) -> (rule7 % int2))) -> (rule3 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
The squirrel visits the tiger.
True
6
proof
[(((triple6 ((triple6 ((triple6) -> rule7)) -> rule3)) -> rule5))]
("squirrel" "visits" "tiger" "+")
((triple6 ((triple6 ((triple6) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int3
The squirrel does not visit the tiger.
False
6
inv-proof
[(((triple6 ((triple6 ((triple6) -> rule7)) -> rule3)) -> rule5))]
("squirrel" "visits" "tiger" "-")
((triple6 ((triple6 ((triple6) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int3
The squirrel is young.
True
7
proof
[(((((triple6 ((triple6 ((triple6) -> rule7)) -> rule3)) -> rule5)) -> rule2))]
("squirrel" "is" "young" "+")
((((triple6 ((triple6 ((triple6) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
int3
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int4
The squirrel is not young.
False
7
inv-proof
[(((((triple6 ((triple6 ((triple6) -> rule7)) -> rule3)) -> rule5)) -> rule2))]
("squirrel" "is" "young" "-")
((((triple6 ((triple6 ((triple6) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
int3
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int4
The squirrel sees the mouse.
True
8
proof
[(((((((triple6 ((triple6 ((triple6) -> rule7)) -> rule3)) -> rule5)) -> rule2)) -> rule6))]
("squirrel" "sees" "mouse" "+")
((((((triple6 ((triple6 ((triple6) -> (rule7 % int5))) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int3
The squirrel is rough.
("squirrel" "is" "rough" "+")
int4
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int5
The squirrel does not see the mouse.
False
8
inv-proof
[(((((((triple6 ((triple6 ((triple6) -> rule7)) -> rule3)) -> rule5)) -> rule2)) -> rule6))]
("squirrel" "sees" "mouse" "-")
((((((triple6 ((triple6 ((triple6) -> (rule7 % int5))) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int3
The squirrel is rough.
("squirrel" "is" "rough" "+")
int4
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int5
The cat does not visit the tiger.
Unknown
inv-rconc
[@1: The cat visits the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "visits" "tiger" "-")
The mouse eats the tiger.
Unknown
rconc
[@1: The mouse eats the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "eats" "tiger" "+")
The tiger does not see the mouse.
Unknown
inv-rconc
[@3: The tiger sees the mouse.[CWA. Example of deepest failure = (rule6 <- rule2 <- rule5 <- FAIL)]]
("tiger" "sees" "mouse" "-")
The tiger is young.
Unknown
rconc
[@2: The tiger is young.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("tiger" "is" "young" "+")
The squirrel does not eat the tiger.
Unknown
inv-rconc
[@1: The squirrel eats the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "eats" "tiger" "-")
The cat sees the mouse.
Unknown
rconc
[@3: The cat sees the mouse.[CWA. Example of deepest failure = (rule6 <- rule2 <- rule5 <- FAIL)]]
("cat" "sees" "mouse" "+")
The tiger does not visit the mouse.
Unknown
inv-random
[@0: The tiger visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "mouse" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The squirrel visits the cat.
Unknown
random
[@0: The squirrel visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "cat" "+")
The mouse does not eat the cat.
Unknown
inv-random
[@0: The mouse eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "cat" "-")
The cat is cold.
Unknown
random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "+")
@0: The cat eats the tiger.[(triple1)] The cat is blue.[(triple2)] The mouse is cold.[(triple3)] The mouse is rough.[(triple4 OR ((triple3 ((triple3) -> rule7)) -> rule3))] The mouse visits the tiger.[(triple5 OR ((triple3 triple4) -> rule5) OR ((triple3 ((triple3 ((triple3) -> rule7)) -> rule3)) -> rule5))] The squirrel is cold.[(triple6)] The squirrel sees the tiger.[(triple7)] The tiger eats the mouse.[(triple8)] The tiger eats the squirrel.[(triple9)] The tiger is rough.[(triple10)] The tiger visits the cat.[(triple11)] @1: The mouse is young.[(((triple5) -> rule2) OR ((((triple3 triple4) -> rule5)) -> rule2) OR ((((triple3 ((triple3 ((triple3) -> rule7)) -> rule3)) -> rule5)) -> rule2))] The mouse sees the squirrel.[(((triple3) -> rule7) OR ((triple4) -> rule1))] The squirrel sees the squirrel.[(((triple6) -> rule7))] The tiger eats the tiger.[(((triple9) -> rule4))] The tiger sees the squirrel.[(((triple10) -> rule1))] @2: The mouse sees the mouse.[(((((triple5) -> rule2)) -> rule6) OR ((((((triple3 triple4) -> rule5)) -> rule2)) -> rule6) OR ((((((triple3 ((triple3 ((triple3) -> rule7)) -> rule3)) -> rule5)) -> rule2)) -> rule6))] The squirrel is rough.[(((triple6 ((triple6) -> rule7)) -> rule3))] @3: The squirrel visits the tiger.[(((triple6 ((triple6 ((triple6) -> rule7)) -> rule3)) -> rule5))] @4: The squirrel is young.[(((((triple6 ((triple6 ((triple6) -> rule7)) -> rule3)) -> rule5)) -> rule2))] @5: The squirrel sees the mouse.[(((((((triple6 ((triple6 ((triple6) -> rule7)) -> rule3)) -> rule5)) -> rule2)) -> rule6))]
The cat eats the tiger.
("cat" "eats" "tiger" "+")
triple1
The cat is blue.
("cat" "is" "blue" "+")
triple2
The mouse is cold.
("mouse" "is" "cold" "+")
triple3
The mouse is rough.
("mouse" "is" "rough" "+")
triple4
((triple3 ((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple5
((triple3 triple4) -> (rule5 % int1))
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int1
((triple3 ((triple3 ((triple3) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int3
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple6
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
triple7
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple8
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
triple9
The tiger is rough.
("tiger" "is" "rough" "+")
triple10
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple11
The mouse is young.
("mouse" "is" "young" "+")
((triple5) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
((((triple3 triple4) -> (rule5 % int2))) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int2
((((triple3 ((triple3 ((triple3) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int4
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
((triple3) -> (rule7 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
((triple4) -> (rule1 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((triple6) -> (rule7 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((triple9) -> (rule4 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
((triple10) -> (rule1 % int1))
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((((triple5) -> (rule2 % int2))) -> (rule6 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
((((((triple3 triple4) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int3
((((((triple3 ((triple3 ((triple3) -> (rule7 % int5))) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int3
The mouse is rough.
("mouse" "is" "rough" "+")
int4
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int5
The squirrel is rough.
("squirrel" "is" "rough" "+")
((triple6 ((triple6) -> (rule7 % int2))) -> (rule3 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
((triple6 ((triple6 ((triple6) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int3
The squirrel is young.
("squirrel" "is" "young" "+")
((((triple6 ((triple6 ((triple6) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
int3
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int4
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
((((((triple6 ((triple6 ((triple6) -> (rule7 % int5))) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int3
The squirrel is rough.
("squirrel" "is" "rough" "+")
int4
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int5