The cat is not cold. The cat is green. The cat is kind. The cat is nice. The cat is young. The cat likes the cow. The cat needs the cow. The cat does not visit the cow. The cow is cold. The cow is not green. The cow is not kind. The cow is nice. The cow is young. The cow likes the cat. The cow needs the cat. The cow visits the cat. If something needs the cow and it is nice then the cow is cold. If something is young then it needs the cat. If something is young and cold then it likes the cow.
The cat is not cold.
("cat" "is" "cold" "-")
The cat is green.
("cat" "is" "green" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is young.
("cat" "is" "young" "+")
The cat likes the cow.
("cat" "likes" "cow" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cat does not visit the cow.
("cat" "visits" "cow" "-")
The cow is cold.
("cow" "is" "cold" "+")
The cow is not green.
("cow" "is" "green" "-")
The cow is not kind.
("cow" "is" "kind" "-")
The cow is nice.
("cow" "is" "nice" "+")
The cow is young.
("cow" "is" "young" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
If something needs the cow and it is nice then the cow is cold.
((("something" "needs" "cow" "+") ("something" "is" "nice" "+")) -> ("cow" "is" "cold" "+"))
If something is young then it needs the cat.
((("something" "is" "young" "+")) -> ("something" "needs" "cat" "+"))
If something is young and cold then it likes the cow.
((("something" "is" "young" "+") ("something" "is" "cold" "+")) -> ("something" "likes" "cow" "+"))
The cat is not cold.
True
1
proof
[(triple1)]
("cat" "is" "cold" "-")
triple1
The cow is not nice.
False
1
inv-proof
[(triple12)]
("cow" "is" "nice" "-")
triple12
The cat needs the cat.
True
2
proof
[(((triple5) -> rule2))]
("cat" "needs" "cat" "+")
((triple5) -> (rule2 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cow does not like the cow.
False
3
inv-proof
[(((triple13 triple9) -> rule3) OR ((triple13 ((triple7 triple4) -> rule1)) -> rule3))]
("cow" "likes" "cow" "-")
((triple13 triple9) -> (rule3 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
((triple13 ((triple7 triple4) -> (rule1 % int2))) -> (rule3 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
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 visits the cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "+")
The cat does not like the cat.
Unknown
inv-random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
@0: The cat does not visit the cow.[(triple8)] The cat is green.[(triple2)] The cat is kind.[(triple3)] The cat is nice.[(triple4)] The cat is not cold.[(triple1)] The cat is young.[(triple5)] The cat likes the cow.[(triple6)] The cat needs the cow.[(triple7)] The cow is cold.[(triple9 OR ((triple7 triple4) -> rule1))] The cow is nice.[(triple12)] The cow is not green.[(triple10)] The cow is not kind.[(triple11)] The cow is young.[(triple13)] The cow likes the cat.[(triple14)] The cow needs the cat.[(triple15 OR ((triple13) -> rule2))] The cow visits the cat.[(triple16)] @1: The cat needs the cat.[(((triple5) -> rule2))] The cow likes the cow.[(((triple13 triple9) -> rule3) OR ((triple13 ((triple7 triple4) -> rule1)) -> rule3))]
The cat does not visit the cow.
("cat" "visits" "cow" "-")
triple8
The cat is green.
("cat" "is" "green" "+")
triple2
The cat is kind.
("cat" "is" "kind" "+")
triple3
The cat is nice.
("cat" "is" "nice" "+")
triple4
The cat is not cold.
("cat" "is" "cold" "-")
triple1
The cat is young.
("cat" "is" "young" "+")
triple5
The cat likes the cow.
("cat" "likes" "cow" "+")
triple6
The cat needs the cow.
("cat" "needs" "cow" "+")
triple7
The cow is cold.
("cow" "is" "cold" "+")
triple9
((triple7 triple4) -> (rule1 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
triple12
The cow is not green.
("cow" "is" "green" "-")
triple10
The cow is not kind.
("cow" "is" "kind" "-")
triple11
The cow is young.
("cow" "is" "young" "+")
triple13
The cow likes the cat.
("cow" "likes" "cat" "+")
triple14
The cow needs the cat.
("cow" "needs" "cat" "+")
triple15
((triple13) -> (rule2 % int1))
The cow needs the cat.
("cow" "needs" "cat" "+")
int1
The cow visits the cat.
("cow" "visits" "cat" "+")
triple16
The cat needs the cat.
("cat" "needs" "cat" "+")
((triple5) -> (rule2 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
((triple13 triple9) -> (rule3 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
((triple13 ((triple7 triple4) -> (rule1 % int2))) -> (rule3 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2