The cow likes the squirrel. The squirrel visits the cow. If the cow needs the squirrel and the cow visits the squirrel then the cow likes the squirrel. If something is big then it visits the squirrel. If something visits the cow then the cow likes the squirrel. If something visits the cow and the cow likes the squirrel then the cow visits the squirrel. If something visits the squirrel then it needs the squirrel. If something is red then it likes the squirrel. If something is round and it likes the cow then it needs the cow. If something visits the squirrel and the squirrel needs the cow then the cow needs the squirrel.
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
If the cow needs the squirrel and the cow visits the squirrel then the cow likes the squirrel.
((("cow" "needs" "squirrel" "+") ("cow" "visits" "squirrel" "+")) -> ("cow" "likes" "squirrel" "+"))
If something is big then it visits the squirrel.
((("something" "is" "big" "+")) -> ("something" "visits" "squirrel" "+"))
If something visits the cow then the cow likes the squirrel.
((("something" "visits" "cow" "+")) -> ("cow" "likes" "squirrel" "+"))
If something visits the cow and the cow likes the squirrel then the cow visits the squirrel.
((("something" "visits" "cow" "+") ("cow" "likes" "squirrel" "+")) -> ("cow" "visits" "squirrel" "+"))
If something visits the squirrel then it needs the squirrel.
((("something" "visits" "squirrel" "+")) -> ("something" "needs" "squirrel" "+"))
If something is red then it likes the squirrel.
((("something" "is" "red" "+")) -> ("something" "likes" "squirrel" "+"))
If something is round and it likes the cow then it needs the cow.
((("something" "is" "round" "+") ("something" "likes" "cow" "+")) -> ("something" "needs" "cow" "+"))
If something visits the squirrel and the squirrel needs the cow then the cow needs the squirrel.
((("something" "visits" "squirrel" "+") ("squirrel" "needs" "cow" "+")) -> ("cow" "needs" "squirrel" "+"))
The cow likes the squirrel.
True
1
proof
[(triple1 OR ((triple2) -> rule3))]
("cow" "likes" "squirrel" "+")
triple1
((triple2) -> (rule3 % int1))
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
int1
The squirrel does not visit the cow.
False
1
inv-proof
[(triple2)]
("squirrel" "visits" "cow" "-")
triple2
The cow visits the squirrel.
True
3
proof
[(((triple2 triple1) -> rule4) OR ((triple2 ((triple2) -> rule3)) -> rule4))]
("cow" "visits" "squirrel" "+")
((triple2 triple1) -> (rule4 % int1))
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int1
((triple2 ((triple2) -> (rule3 % int2))) -> (rule4 % int1))
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int1
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
int2
The cow does not visit the squirrel.
False
3
inv-proof
[(((triple2 triple1) -> rule4) OR ((triple2 ((triple2) -> rule3)) -> rule4))]
("cow" "visits" "squirrel" "-")
((triple2 triple1) -> (rule4 % int1))
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int1
((triple2 ((triple2) -> (rule3 % int2))) -> (rule4 % int1))
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int1
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
int2
The cow needs the squirrel.
True
4
proof
[(((((triple2 triple1) -> rule4)) -> rule5) OR ((((triple2 ((triple2) -> rule3)) -> rule4)) -> rule5))]
("cow" "needs" "squirrel" "+")
((((triple2 triple1) -> (rule4 % int2))) -> (rule5 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int2
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int2
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
int3
The cow does not need the squirrel.
False
4
inv-proof
[(((((triple2 triple1) -> rule4)) -> rule5) OR ((((triple2 ((triple2) -> rule3)) -> rule4)) -> rule5))]
("cow" "needs" "squirrel" "-")
((((triple2 triple1) -> (rule4 % int2))) -> (rule5 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int2
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int2
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
int3
The squirrel does not visit the squirrel.
Unknown
inv-rconc
[@1: The squirrel visits the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "visits" "squirrel" "-")
The cow needs the cow.
Unknown
rconc
[@1: The cow needs the cow.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cow" "needs" "cow" "+")
The squirrel does not need the squirrel.
Unknown
inv-rconc
[@2: The squirrel needs the squirrel.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("squirrel" "needs" "squirrel" "-")
The cow is kind.
Unknown
random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "+")
The squirrel is not rough.
Unknown
inv-random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "-")
The squirrel is kind.
Unknown
random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "+")
@0: The cow likes the squirrel.[(triple1 OR ((triple2) -> rule3))] The squirrel visits the cow.[(triple2)] @1: The cow visits the squirrel.[(((triple2 triple1) -> rule4) OR ((triple2 ((triple2) -> rule3)) -> rule4))] @2: The cow needs the squirrel.[(((((triple2 triple1) -> rule4)) -> rule5) OR ((((triple2 ((triple2) -> rule3)) -> rule4)) -> rule5))]
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
triple1
((triple2) -> (rule3 % int1))
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
int1
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
triple2
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
((triple2 triple1) -> (rule4 % int1))
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int1
((triple2 ((triple2) -> (rule3 % int2))) -> (rule4 % int1))
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int1
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
int2
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
((((triple2 triple1) -> (rule4 % int2))) -> (rule5 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int2
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int2
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
int3