The cow likes the squirrel. The dog is not green. The dog likes the cow. The dog needs the cow. The dog needs the squirrel. The squirrel chases the dog. The squirrel is blue. The squirrel is not cold. The squirrel is young. The squirrel needs the cow. If something likes the cow and it does not need the cow then it likes the squirrel. If something needs the cow and it is young then the cow likes the squirrel. If the squirrel is green then the squirrel likes the cow. If the squirrel is young then the squirrel is green. If something is cold and it likes the dog then the dog likes the cow. If something needs the cow and it does not need the squirrel then it is blue. If something likes the dog then the dog chases the cow. If something needs the cow and the cow is not red then it is young.
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
The dog is not green.
("dog" "is" "green" "-")
The dog likes the cow.
("dog" "likes" "cow" "+")
The dog needs the cow.
("dog" "needs" "cow" "+")
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is not cold.
("squirrel" "is" "cold" "-")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
If something likes the cow and it does not need the cow then it likes the squirrel.
((("something" "likes" "cow" "+") ("something" "needs" "cow" "~")) -> ("something" "likes" "squirrel" "+"))
If something needs the cow and it is young then the cow likes the squirrel.
((("something" "needs" "cow" "+") ("something" "is" "young" "+")) -> ("cow" "likes" "squirrel" "+"))
If the squirrel is green then the squirrel likes the cow.
((("squirrel" "is" "green" "+")) -> ("squirrel" "likes" "cow" "+"))
If the squirrel is young then the squirrel is green.
((("squirrel" "is" "young" "+")) -> ("squirrel" "is" "green" "+"))
If something is cold and it likes the dog then the dog likes the cow.
((("something" "is" "cold" "+") ("something" "likes" "dog" "+")) -> ("dog" "likes" "cow" "+"))
If something needs the cow and it does not need the squirrel then it is blue.
((("something" "needs" "cow" "+") ("something" "needs" "squirrel" "~")) -> ("something" "is" "blue" "+"))
If something likes the dog then the dog chases the cow.
((("something" "likes" "dog" "+")) -> ("dog" "chases" "cow" "+"))
If something needs the cow and the cow is not red then it is young.
((("something" "needs" "cow" "+") ("cow" "is" "red" "~")) -> ("something" "is" "young" "+"))
The squirrel needs the cow.
True
1
proof
[(triple10)]
("squirrel" "needs" "cow" "+")
triple10
The squirrel does not need the cow.
False
1
inv-proof
[(triple10)]
("squirrel" "needs" "cow" "-")
triple10
The squirrel is green.
True
2
proof
[(((triple9) -> rule4))]
("squirrel" "is" "green" "+")
((triple9) -> (rule4 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is not green.
False
2
inv-proof
[(((triple9) -> rule4))]
("squirrel" "is" "green" "-")
((triple9) -> (rule4 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel likes the cow.
True
3
proof
[(((((triple9) -> rule4)) -> rule3))]
("squirrel" "likes" "cow" "+")
((((triple9) -> (rule4 % int2))) -> (rule3 % int1))
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The squirrel does not like the cow.
False
3
inv-proof
[(((((triple9) -> rule4)) -> rule3))]
("squirrel" "likes" "cow" "-")
((((triple9) -> (rule4 % int2))) -> (rule3 % int1))
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The dog does not chase the cow.
Unknown
inv-rconc
[@1: The dog chases the cow.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "chases" "cow" "-")
The cow is blue.
Unknown
rconc
[@1: The cow is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "is" "blue" "+")
The dog is not blue.
Unknown
inv-rconc
[@1: The dog is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "is" "blue" "-")
The dog is cold.
Unknown
random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "+")
The cow does not need the cow.
Unknown
inv-random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "-")
The cow is cold.
Unknown
random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "+")
@0: The cow likes the squirrel.[(triple1 OR ((triple10 triple9) -> rule2))] The dog is not green.[(triple2)] The dog likes the cow.[(triple3)] The dog needs the cow.[(triple4)] The dog needs the squirrel.[(triple5)] The squirrel chases the dog.[(triple6)] The squirrel is blue.[(triple7)] The squirrel is not cold.[(triple8)] The squirrel is young.[(triple9)] The squirrel needs the cow.[(triple10)] @1: The squirrel is green.[(((triple9) -> rule4))] @2: The squirrel likes the cow.[(((((triple9) -> rule4)) -> rule3))]
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
triple1
((triple10 triple9) -> (rule2 % int1))
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
int1
The dog is not green.
("dog" "is" "green" "-")
triple2
The dog likes the cow.
("dog" "likes" "cow" "+")
triple3
The dog needs the cow.
("dog" "needs" "cow" "+")
triple4
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
triple5
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
triple6
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple7
The squirrel is not cold.
("squirrel" "is" "cold" "-")
triple8
The squirrel is young.
("squirrel" "is" "young" "+")
triple9
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
triple10
The squirrel is green.
("squirrel" "is" "green" "+")
((triple9) -> (rule4 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
((((triple9) -> (rule4 % int2))) -> (rule3 % int1))
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2