The cow is round. The cow needs the mouse. The cow needs the tiger. The cow visits the squirrel. The mouse likes the cow. The mouse needs the tiger. The mouse visits the cow. The squirrel is cold. The squirrel is nice. The squirrel needs the cow. The squirrel visits the mouse. The tiger is cold. The tiger is red. The tiger likes the cow. The tiger visits the mouse. The tiger visits the squirrel. If something is red then it is green. Cold things are nice. If something is nice then it likes the mouse. If the tiger likes the mouse then the tiger likes the cow. If something is red and it likes the cow then it is green. If something is red and it likes the mouse then the mouse is cold. If the squirrel needs the cow and the cow likes the squirrel then the squirrel visits the tiger. If something needs the cow then it likes the tiger. If something is red and it likes the cow then it visits the tiger.
The cow is round.
("cow" "is" "round" "+")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The mouse visits the cow.
("mouse" "visits" "cow" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger likes the cow.
("tiger" "likes" "cow" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If something is red then it is green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
Cold things are nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If something is nice then it likes the mouse.
((("something" "is" "nice" "+")) -> ("something" "likes" "mouse" "+"))
If the tiger likes the mouse then the tiger likes the cow.
((("tiger" "likes" "mouse" "+")) -> ("tiger" "likes" "cow" "+"))
If something is red and it likes the cow then it is green.
((("something" "is" "red" "+") ("something" "likes" "cow" "+")) -> ("something" "is" "green" "+"))
If something is red and it likes the mouse then the mouse is cold.
((("something" "is" "red" "+") ("something" "likes" "mouse" "+")) -> ("mouse" "is" "cold" "+"))
If the squirrel needs the cow and the cow likes the squirrel then the squirrel visits the tiger.
((("squirrel" "needs" "cow" "+") ("cow" "likes" "squirrel" "+")) -> ("squirrel" "visits" "tiger" "+"))
If something needs the cow then it likes the tiger.
((("something" "needs" "cow" "+")) -> ("something" "likes" "tiger" "+"))
If something is red and it likes the cow then it visits the tiger.
((("something" "is" "red" "+") ("something" "likes" "cow" "+")) -> ("something" "visits" "tiger" "+"))
The tiger likes the cow.
True
1
proof
[(triple14 OR ((((((triple12) -> rule2)) -> rule3)) -> rule4))]
("tiger" "likes" "cow" "+")
triple14
((((((triple12) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
The cow is not round.
False
1
inv-proof
[(triple1)]
("cow" "is" "round" "-")
triple1
The tiger is nice.
True
2
proof
[(((triple12) -> rule2))]
("tiger" "is" "nice" "+")
((triple12) -> (rule2 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The squirrel does not like the mouse.
False
2
inv-proof
[(((triple9) -> rule3) OR ((((triple8) -> rule2)) -> rule3))]
("squirrel" "likes" "mouse" "-")
((triple9) -> (rule3 % int1))
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The tiger likes the mouse.
True
3
proof
[(((((triple12) -> rule2)) -> rule3))]
("tiger" "likes" "mouse" "+")
((((triple12) -> (rule2 % int2))) -> (rule3 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger does not like the mouse.
False
3
inv-proof
[(((((triple12) -> rule2)) -> rule3))]
("tiger" "likes" "mouse" "-")
((((triple12) -> (rule2 % int2))) -> (rule3 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The mouse is cold.
True
5
proof
[(((triple13 ((((triple12) -> rule2)) -> rule3)) -> rule6))]
("mouse" "is" "cold" "+")
((triple13 ((((triple12) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
The mouse is not cold.
False
5
inv-proof
[(((triple13 ((((triple12) -> rule2)) -> rule3)) -> rule6))]
("mouse" "is" "cold" "-")
((triple13 ((((triple12) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
The mouse is nice.
True
6
proof
[(((((triple13 ((((triple12) -> rule2)) -> rule3)) -> rule6)) -> rule2))]
("mouse" "is" "nice" "+")
((((triple13 ((((triple12) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int3
The tiger is nice.
("tiger" "is" "nice" "+")
int4
The mouse is not nice.
False
6
inv-proof
[(((((triple13 ((((triple12) -> rule2)) -> rule3)) -> rule6)) -> rule2))]
("mouse" "is" "nice" "-")
((((triple13 ((((triple12) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int3
The tiger is nice.
("tiger" "is" "nice" "+")
int4
The mouse likes the mouse.
True
7
proof
[(((((((triple13 ((((triple12) -> rule2)) -> rule3)) -> rule6)) -> rule2)) -> rule3))]
("mouse" "likes" "mouse" "+")
((((((triple13 ((((triple12) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int4
The tiger is nice.
("tiger" "is" "nice" "+")
int5
The mouse does not like the mouse.
False
7
inv-proof
[(((((((triple13 ((((triple12) -> rule2)) -> rule3)) -> rule6)) -> rule2)) -> rule3))]
("mouse" "likes" "mouse" "-")
((((((triple13 ((((triple12) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int4
The tiger is nice.
("tiger" "is" "nice" "+")
int5
The cow does not visit the tiger.
Unknown
inv-rconc
[@1: The cow visits the tiger.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("cow" "visits" "tiger" "-")
The squirrel visits the tiger.
Unknown
rconc
[@1: The squirrel visits the tiger.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "visits" "tiger" "+")
The cow does not like the mouse.
Unknown
inv-rconc
[@2: The cow likes the mouse.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("cow" "likes" "mouse" "-")
The cow is nice.
Unknown
rconc
[@1: The cow is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "nice" "+")
The mouse does not visit the tiger.
Unknown
inv-rconc
[@1: The mouse visits the tiger.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("mouse" "visits" "tiger" "-")
The cow likes the tiger.
Unknown
rconc
[@1: The cow likes the tiger.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "likes" "tiger" "+")
The cow does not like the squirrel.
Unknown
inv-random
[@0: The cow likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "squirrel" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
The tiger does not need the cow.
Unknown
inv-random
[@0: The tiger needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "cow" "-")
The squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
The squirrel does not need the tiger.
Unknown
inv-random
[@0: The squirrel needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "tiger" "-")
The squirrel visits the cow.
Unknown
random
[@0: The squirrel visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "cow" "+")
@0: The cow is round.[(triple1)] The cow needs the mouse.[(triple2)] The cow needs the tiger.[(triple3)] The cow visits the squirrel.[(triple4)] The mouse likes the cow.[(triple5)] The mouse needs the tiger.[(triple6)] The mouse visits the cow.[(triple7)] The squirrel is cold.[(triple8)] The squirrel is nice.[(triple9 OR ((triple8) -> rule2))] The squirrel needs the cow.[(triple10)] The squirrel visits the mouse.[(triple11)] The tiger is cold.[(triple12)] The tiger is red.[(triple13)] The tiger likes the cow.[(triple14 OR ((((((triple12) -> rule2)) -> rule3)) -> rule4))] The tiger visits the mouse.[(triple15)] The tiger visits the squirrel.[(triple16)] @1: The squirrel likes the mouse.[(((triple9) -> rule3) OR ((((triple8) -> rule2)) -> rule3))] The squirrel likes the tiger.[(((triple10) -> rule8))] The tiger is green.[(((triple13) -> rule1) OR ((triple13 triple14) -> rule5) OR ((triple13 ((((((triple12) -> rule2)) -> rule3)) -> rule4)) -> rule5))] The tiger is nice.[(((triple12) -> rule2))] The tiger visits the tiger.[(((triple13 triple14) -> rule9) OR ((triple13 ((((((triple12) -> rule2)) -> rule3)) -> rule4)) -> rule9))] @2: The tiger likes the mouse.[(((((triple12) -> rule2)) -> rule3))] @3: The mouse is cold.[(((triple13 ((((triple12) -> rule2)) -> rule3)) -> rule6))] @4: The mouse is nice.[(((((triple13 ((((triple12) -> rule2)) -> rule3)) -> rule6)) -> rule2))] @5: The mouse likes the mouse.[(((((((triple13 ((((triple12) -> rule2)) -> rule3)) -> rule6)) -> rule2)) -> rule3))]
The cow is round.
("cow" "is" "round" "+")
triple1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple2
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple3
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
triple4
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple5
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple6
The mouse visits the cow.
("mouse" "visits" "cow" "+")
triple7
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple8
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple9
((triple8) -> (rule2 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
triple10
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
triple11
The tiger is cold.
("tiger" "is" "cold" "+")
triple12
The tiger is red.
("tiger" "is" "red" "+")
triple13
The tiger likes the cow.
("tiger" "likes" "cow" "+")
triple14
((((((triple12) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple15
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple16
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
((triple9) -> (rule3 % int1))
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
((triple10) -> (rule8 % int1))
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
((triple13) -> (rule1 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
((triple13 triple14) -> (rule5 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
((triple13 ((((((triple12) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int2
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int3
The tiger is nice.
("tiger" "is" "nice" "+")
int4
The tiger is nice.
("tiger" "is" "nice" "+")
((triple12) -> (rule2 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((triple13 triple14) -> (rule9 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
((triple13 ((((((triple12) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int2
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int3
The tiger is nice.
("tiger" "is" "nice" "+")
int4
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
((((triple12) -> (rule2 % int2))) -> (rule3 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
((triple13 ((((triple12) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
The mouse is nice.
("mouse" "is" "nice" "+")
((((triple13 ((((triple12) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int3
The tiger is nice.
("tiger" "is" "nice" "+")
int4
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((((((triple13 ((((triple12) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int4
The tiger is nice.
("tiger" "is" "nice" "+")
int5