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