The cow is blue. The cow needs the dog. The cow needs the squirrel. The cow sees the dog. The dog is big. The dog needs the cow. The dog needs the squirrel. The dog sees the cow. The squirrel is nice. The squirrel visits the dog. If the dog needs the cow then the cow is big. If someone is big then they visit the dog. If the cow is green then the cow needs the squirrel. If the cow needs the squirrel and the cow visits the dog then the cow sees the squirrel. If someone visits the squirrel then the squirrel is green. If someone sees the cow and they visit the cow then they visit the dog.
The cow is blue.
("cow" "is" "blue" "+")
The cow needs the dog.
("cow" "needs" "dog" "+")
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
The cow sees the dog.
("cow" "sees" "dog" "+")
The dog is big.
("dog" "is" "big" "+")
The dog needs the cow.
("dog" "needs" "cow" "+")
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
The dog sees the cow.
("dog" "sees" "cow" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
If the dog needs the cow then the cow is big.
((("dog" "needs" "cow" "+")) -> ("cow" "is" "big" "+"))
If someone is big then they visit the dog.
((("someone" "is" "big" "+")) -> ("someone" "visits" "dog" "+"))
If the cow is green then the cow needs the squirrel.
((("cow" "is" "green" "+")) -> ("cow" "needs" "squirrel" "+"))
If the cow needs the squirrel and the cow visits the dog then the cow sees the squirrel.
((("cow" "needs" "squirrel" "+") ("cow" "visits" "dog" "+")) -> ("cow" "sees" "squirrel" "+"))
If someone visits the squirrel then the squirrel is green.
((("someone" "visits" "squirrel" "+")) -> ("squirrel" "is" "green" "+"))
If someone sees the cow and they visit the cow then they visit the dog.
((("someone" "sees" "cow" "+") ("someone" "visits" "cow" "+")) -> ("someone" "visits" "dog" "+"))
The cow needs the dog.
True
1
proof
[(triple2)]
("cow" "needs" "dog" "+")
triple2
The cow does not need the dog.
False
1
inv-proof
[(triple2)]
("cow" "needs" "dog" "-")
triple2
The cow is big.
True
2
proof
[(((triple6) -> rule1))]
("cow" "is" "big" "+")
((triple6) -> (rule1 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The dog does not visit the dog.
False
2
inv-proof
[(((triple5) -> rule2))]
("dog" "visits" "dog" "-")
((triple5) -> (rule2 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The cow visits the dog.
True
3
proof
[(((((triple6) -> rule1)) -> rule2))]
("cow" "visits" "dog" "+")
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow does not visit the dog.
False
3
inv-proof
[(((((triple6) -> rule1)) -> rule2))]
("cow" "visits" "dog" "-")
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow sees the squirrel.
True
5
proof
[(((triple3 ((((triple6) -> rule1)) -> rule2)) -> rule4))]
("cow" "sees" "squirrel" "+")
((triple3 ((((triple6) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int1
The cow visits the dog.
("cow" "visits" "dog" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
The cow does not see the squirrel.
False
5
inv-proof
[(((triple3 ((((triple6) -> rule1)) -> rule2)) -> rule4))]
("cow" "sees" "squirrel" "-")
((triple3 ((((triple6) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int1
The cow visits the dog.
("cow" "visits" "dog" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
The squirrel is not green.
Unknown
inv-rconc
[@1: The squirrel is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "is" "green" "-")
The squirrel is big.
Unknown
random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "+")
The squirrel is not blue.
Unknown
inv-random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
The squirrel does not need the cow.
Unknown
inv-random
[@0: The squirrel needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "cow" "-")
The cow is green.
Unknown
random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "+")
The squirrel does not see the cow.
Unknown
inv-random
[@0: The squirrel sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "cow" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
@0: The cow is blue.[(triple1)] The cow needs the dog.[(triple2)] The cow needs the squirrel.[(triple3)] The cow sees the dog.[(triple4)] The dog is big.[(triple5)] The dog needs the cow.[(triple6)] The dog needs the squirrel.[(triple7)] The dog sees the cow.[(triple8)] The squirrel is nice.[(triple9)] The squirrel visits the dog.[(triple10)] @1: The cow is big.[(((triple6) -> rule1))] The dog visits the dog.[(((triple5) -> rule2))] @2: The cow visits the dog.[(((((triple6) -> rule1)) -> rule2))] @3: The cow sees the squirrel.[(((triple3 ((((triple6) -> rule1)) -> rule2)) -> rule4))]
The cow is blue.
("cow" "is" "blue" "+")
triple1
The cow needs the dog.
("cow" "needs" "dog" "+")
triple2
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
triple3
The cow sees the dog.
("cow" "sees" "dog" "+")
triple4
The dog is big.
("dog" "is" "big" "+")
triple5
The dog needs the cow.
("dog" "needs" "cow" "+")
triple6
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
triple7
The dog sees the cow.
("dog" "sees" "cow" "+")
triple8
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple9
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
triple10
The cow is big.
("cow" "is" "big" "+")
((triple6) -> (rule1 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
((triple5) -> (rule2 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The cow visits the dog.
("cow" "visits" "dog" "+")
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
((triple3 ((((triple6) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int1
The cow visits the dog.
("cow" "visits" "dog" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3