The mouse is round. The squirrel is rough. The squirrel likes the mouse. If someone is round then they like the squirrel. If the mouse visits the squirrel and the mouse likes the squirrel then the squirrel visits the mouse. If someone visits the mouse and the mouse likes the squirrel then they like the squirrel. If someone chases the mouse then they chase the squirrel. If the mouse likes the squirrel then the squirrel chases the mouse. If someone chases the mouse then the mouse visits the squirrel.
The mouse is round.
("mouse" "is" "round" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
If someone is round then they like the squirrel.
((("someone" "is" "round" "+")) -> ("someone" "likes" "squirrel" "+"))
If the mouse visits the squirrel and the mouse likes the squirrel then the squirrel visits the mouse.
((("mouse" "visits" "squirrel" "+") ("mouse" "likes" "squirrel" "+")) -> ("squirrel" "visits" "mouse" "+"))
If someone visits the mouse and the mouse likes the squirrel then they like the squirrel.
((("someone" "visits" "mouse" "+") ("mouse" "likes" "squirrel" "+")) -> ("someone" "likes" "squirrel" "+"))
If someone chases the mouse then they chase the squirrel.
((("someone" "chases" "mouse" "+")) -> ("someone" "chases" "squirrel" "+"))
If the mouse likes the squirrel then the squirrel chases the mouse.
((("mouse" "likes" "squirrel" "+")) -> ("squirrel" "chases" "mouse" "+"))
If someone chases the mouse then the mouse visits the squirrel.
((("someone" "chases" "mouse" "+")) -> ("mouse" "visits" "squirrel" "+"))
The squirrel is rough.
True
1
proof
[(triple2)]
("squirrel" "is" "rough" "+")
triple2
The mouse is not round.
False
1
inv-proof
[(triple1)]
("mouse" "is" "round" "-")
triple1
The mouse likes the squirrel.
True
2
proof
[(((triple1) -> rule1))]
("mouse" "likes" "squirrel" "+")
((triple1) -> (rule1 % int1))
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int1
The mouse does not like the squirrel.
False
2
inv-proof
[(((triple1) -> rule1))]
("mouse" "likes" "squirrel" "-")
((triple1) -> (rule1 % int1))
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int1
The squirrel chases the mouse.
True
3
proof
[(((((triple1) -> rule1)) -> rule5))]
("squirrel" "chases" "mouse" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int1
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int2
The squirrel does not chase the mouse.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule5))]
("squirrel" "chases" "mouse" "-")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int1
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int2
The squirrel chases the squirrel.
True
4
proof
[(((((((triple1) -> rule1)) -> rule5)) -> rule4))]
("squirrel" "chases" "squirrel" "+")
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int2
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int3
The mouse does not visit the squirrel.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule5)) -> rule6))]
("mouse" "visits" "squirrel" "-")
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int1
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int2
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int3
The mouse does not chase the squirrel.
Unknown
inv-rconc
[@1: The mouse chases the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "chases" "squirrel" "-")
The squirrel is nice.
Unknown
random
[@0: The squirrel is nice.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "nice" "+")
The mouse does not like the mouse.
Unknown
inv-random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "-")
The mouse is cold.
Unknown
random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "+")
The mouse does not visit the mouse.
Unknown
inv-random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "-")
The mouse is nice.
Unknown
random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "+")
The mouse is not young.
Unknown
inv-random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "-")
The squirrel is young.
Unknown
random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "+")
@0: The mouse is round.[(triple1)] The squirrel is rough.[(triple2)] The squirrel likes the mouse.[(triple3)] @1: The mouse likes the squirrel.[(((triple1) -> rule1))] @2: The squirrel chases the mouse.[(((((triple1) -> rule1)) -> rule5))] @3: The mouse visits the squirrel.[(((((((triple1) -> rule1)) -> rule5)) -> rule6))] The squirrel chases the squirrel.[(((((((triple1) -> rule1)) -> rule5)) -> rule4))] @4: The squirrel visits the mouse.[(((((((((triple1) -> rule1)) -> rule5)) -> rule6) ((triple1) -> rule1)) -> rule2))] @5: The squirrel likes the squirrel.[(((((((((((triple1) -> rule1)) -> rule5)) -> rule6) ((triple1) -> rule1)) -> rule2) ((triple1) -> rule1)) -> rule3))]
The mouse is round.
("mouse" "is" "round" "+")
triple1
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple2
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
triple3
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
((triple1) -> (rule1 % int1))
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int1
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int1
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int2
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int1
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int2
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int3
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int2
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int3
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
((((((((triple1) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule6 % int2)) ((triple1) -> (rule1 % int4))) -> (rule2 % int1))
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int3
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int4
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
((((((((((triple1) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule6 % int3)) ((triple1) -> (rule1 % int5))) -> (rule2 % int2)) ((triple1) -> (rule1 % int5))) -> (rule3 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int2
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int3
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int4
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int5