The cat eats the cow. The cat is blue. The cat is cold. The cat is kind. The cat is nice. The cat is young. The cat needs the cow. The cat sees the cow. The cow is blue. The cow is nice. The cow needs the cat. The cow sees the cat. If something needs the cow then it needs the cat.
The cat eats the cow.
("cat" "eats" "cow" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is young.
("cat" "is" "young" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cat sees the cow.
("cat" "sees" "cow" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
If something needs the cow then it needs the cat.
((("something" "needs" "cow" "+")) -> ("something" "needs" "cat" "+"))
The cow needs the cat.
True
1
proof
[(triple11)]
("cow" "needs" "cat" "+")
triple11
The cat is not nice.
False
1
inv-proof
[(triple5)]
("cat" "is" "nice" "-")
triple5
The cat needs the cat.
True
2
proof
[(((triple7) -> rule1))]
("cat" "needs" "cat" "+")
((triple7) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat does not need the cat.
False
2
inv-proof
[(((triple7) -> rule1))]
("cat" "needs" "cat" "-")
((triple7) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The cow is cold.
Unknown
random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "+")
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The cow eats the cat.
Unknown
random
[@0: The cow eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cat" "+")
@0: The cat eats the cow.[(triple1)] The cat is blue.[(triple2)] The cat is cold.[(triple3)] The cat is kind.[(triple4)] The cat is nice.[(triple5)] The cat is young.[(triple6)] The cat needs the cow.[(triple7)] The cat sees the cow.[(triple8)] The cow is blue.[(triple9)] The cow is nice.[(triple10)] The cow needs the cat.[(triple11)] The cow sees the cat.[(triple12)] @1: The cat needs the cat.[(((triple7) -> rule1))]
The cat eats the cow.
("cat" "eats" "cow" "+")
triple1
The cat is blue.
("cat" "is" "blue" "+")
triple2
The cat is cold.
("cat" "is" "cold" "+")
triple3
The cat is kind.
("cat" "is" "kind" "+")
triple4
The cat is nice.
("cat" "is" "nice" "+")
triple5
The cat is young.
("cat" "is" "young" "+")
triple6
The cat needs the cow.
("cat" "needs" "cow" "+")
triple7
The cat sees the cow.
("cat" "sees" "cow" "+")
triple8
The cow is blue.
("cow" "is" "blue" "+")
triple9
The cow is nice.
("cow" "is" "nice" "+")
triple10
The cow needs the cat.
("cow" "needs" "cat" "+")
triple11
The cow sees the cat.
("cow" "sees" "cat" "+")
triple12
The cat needs the cat.
("cat" "needs" "cat" "+")
((triple7) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1