The cat is blue. The cat is red. The cat is rough. The cat is round. The cat needs the cow. The cat sees the cow. The cat visits the cow. The cow is blue. The cow is round. The cow needs the cat. The cow sees the cat. The cow visits the cat. If something sees the cow then it needs the cow. If something sees the cat then it sees the cow.
The cat is blue.
("cat" "is" "blue" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is round.
("cat" "is" "round" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cat sees the cow.
("cat" "sees" "cow" "+")
The cat visits the cow.
("cat" "visits" "cow" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is round.
("cow" "is" "round" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
If something sees the cow then it needs the cow.
((("something" "sees" "cow" "+")) -> ("something" "needs" "cow" "+"))
If something sees the cat then it sees the cow.
((("something" "sees" "cat" "+")) -> ("something" "sees" "cow" "+"))
The cow is blue.
True
1
proof
[(triple8)]
("cow" "is" "blue" "+")
triple8
The cow is not blue.
False
1
inv-proof
[(triple8)]
("cow" "is" "blue" "-")
triple8
The cow sees the cow.
True
2
proof
[(((triple11) -> rule2))]
("cow" "sees" "cow" "+")
((triple11) -> (rule2 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow does not see the cow.
False
2
inv-proof
[(((triple11) -> rule2))]
("cow" "sees" "cow" "-")
((triple11) -> (rule2 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow needs the cow.
True
3
proof
[(((((triple11) -> rule2)) -> rule1))]
("cow" "needs" "cow" "+")
((((triple11) -> (rule2 % int2))) -> (rule1 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
int2
The cow does not need the cow.
False
3
inv-proof
[(((((triple11) -> rule2)) -> rule1))]
("cow" "needs" "cow" "-")
((((triple11) -> (rule2 % int2))) -> (rule1 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
int2
The cat is not big.
Unknown
inv-random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "-")
The cow is rough.
Unknown
random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "+")
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The cow is red.
Unknown
random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "+")
The cat does not need the cat.
Unknown
inv-random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "-")
The cow is big.
Unknown
random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "+")
@0: The cat is blue.[(triple1)] The cat is red.[(triple2)] The cat is rough.[(triple3)] The cat is round.[(triple4)] The cat needs the cow.[(triple5 OR ((triple6) -> rule1))] The cat sees the cow.[(triple6)] The cat visits the cow.[(triple7)] The cow is blue.[(triple8)] The cow is round.[(triple9)] The cow needs the cat.[(triple10)] The cow sees the cat.[(triple11)] The cow visits the cat.[(triple12)] @1: The cow sees the cow.[(((triple11) -> rule2))] @2: The cow needs the cow.[(((((triple11) -> rule2)) -> rule1))]
The cat is blue.
("cat" "is" "blue" "+")
triple1
The cat is red.
("cat" "is" "red" "+")
triple2
The cat is rough.
("cat" "is" "rough" "+")
triple3
The cat is round.
("cat" "is" "round" "+")
triple4
The cat needs the cow.
("cat" "needs" "cow" "+")
triple5
((triple6) -> (rule1 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
The cat sees the cow.
("cat" "sees" "cow" "+")
triple6
The cat visits the cow.
("cat" "visits" "cow" "+")
triple7
The cow is blue.
("cow" "is" "blue" "+")
triple8
The cow is round.
("cow" "is" "round" "+")
triple9
The cow needs the cat.
("cow" "needs" "cat" "+")
triple10
The cow sees the cat.
("cow" "sees" "cat" "+")
triple11
The cow visits the cat.
("cow" "visits" "cat" "+")
triple12
The cow sees the cow.
("cow" "sees" "cow" "+")
((triple11) -> (rule2 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
((((triple11) -> (rule2 % int2))) -> (rule1 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
int2