The cat is blue. The cat is kind. The cat is red. The cat is rough. The cat is young. The cat likes the cow. The cat sees the cow. The cat visits the cow. The cow is blue. The cow is kind. The cow likes the cat. The cow visits the cat. Young people are rough. If someone sees the cat then they are kind. If the cat sees the cow and the cow sees the cat then the cat visits the cow. If someone sees the cow then they are young. If someone visits the cow and the cow likes the cat then they are young. If the cat visits the cow and the cow visits the cat then the cat likes the cow. If someone visits the cat and they see the cow then the cat sees the cow. If someone likes the cat then they visit the cow.
The cat is blue.
("cat" "is" "blue" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is young.
("cat" "is" "young" "+")
The cat likes the cow.
("cat" "likes" "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 kind.
("cow" "is" "kind" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
Young people are rough.
((("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
If someone sees the cat then they are kind.
((("someone" "sees" "cat" "+")) -> ("someone" "is" "kind" "+"))
If the cat sees the cow and the cow sees the cat then the cat visits the cow.
((("cat" "sees" "cow" "+") ("cow" "sees" "cat" "+")) -> ("cat" "visits" "cow" "+"))
If someone sees the cow then they are young.
((("someone" "sees" "cow" "+")) -> ("someone" "is" "young" "+"))
If someone visits the cow and the cow likes the cat then they are young.
((("someone" "visits" "cow" "+") ("cow" "likes" "cat" "+")) -> ("someone" "is" "young" "+"))
If the cat visits the cow and the cow visits the cat then the cat likes the cow.
((("cat" "visits" "cow" "+") ("cow" "visits" "cat" "+")) -> ("cat" "likes" "cow" "+"))
If someone visits the cat and they see the cow then the cat sees the cow.
((("someone" "visits" "cat" "+") ("someone" "sees" "cow" "+")) -> ("cat" "sees" "cow" "+"))
If someone likes the cat then they visit the cow.
((("someone" "likes" "cat" "+")) -> ("someone" "visits" "cow" "+"))
The cow is blue.
True
1
proof
[(triple9)]
("cow" "is" "blue" "+")
triple9
The cat is not young.
False
1
inv-proof
[(triple5 OR ((triple7) -> rule4) OR ((triple8 triple11) -> rule5))]
("cat" "is" "young" "-")
triple5
((triple7) -> (rule4 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
((triple8 triple11) -> (rule5 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cow visits the cow.
True
2
proof
[(((triple11) -> rule8))]
("cow" "visits" "cow" "+")
((triple11) -> (rule8 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow does not visit the cow.
False
2
inv-proof
[(((triple11) -> rule8))]
("cow" "visits" "cow" "-")
((triple11) -> (rule8 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow is young.
True
4
proof
[(((((triple11) -> rule8) triple11) -> rule5))]
("cow" "is" "young" "+")
((((triple11) -> (rule8 % int2)) triple11) -> (rule5 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow is not young.
False
4
inv-proof
[(((((triple11) -> rule8) triple11) -> rule5))]
("cow" "is" "young" "-")
((((triple11) -> (rule8 % int2)) triple11) -> (rule5 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow is rough.
True
5
proof
[(((((((triple11) -> rule8) triple11) -> rule5)) -> rule1))]
("cow" "is" "rough" "+")
((((((triple11) -> (rule8 % int3)) triple11) -> (rule5 % int2))) -> (rule1 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
int3
The cow is not rough.
False
5
inv-proof
[(((((((triple11) -> rule8) triple11) -> rule5)) -> rule1))]
("cow" "is" "rough" "-")
((((((triple11) -> (rule8 % int3)) triple11) -> (rule5 % int2))) -> (rule1 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
int3
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 cow likes the cow.
Unknown
random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "+")
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 sees the cat.
Unknown
random
[@0: The cow sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cat" "+")
The cow is not red.
Unknown
inv-random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
@0: The cat is blue.[(triple1)] The cat is kind.[(triple2)] The cat is red.[(triple3)] The cat is rough.[(triple4 OR ((triple5) -> rule1) OR ((((triple7) -> rule4)) -> rule1) OR ((((triple8 triple11) -> rule5)) -> rule1))] The cat is young.[(triple5 OR ((triple7) -> rule4) OR ((triple8 triple11) -> rule5))] The cat likes the cow.[(triple6 OR ((triple8 triple12) -> rule6))] The cat sees the cow.[(triple7)] The cat visits the cow.[(triple8)] The cow is blue.[(triple9)] The cow is kind.[(triple10)] The cow likes the cat.[(triple11)] The cow visits the cat.[(triple12)] @1: The cow visits the cow.[(((triple11) -> rule8))] @2: The cow is young.[(((((triple11) -> rule8) triple11) -> rule5))] @3: The cow is rough.[(((((((triple11) -> rule8) triple11) -> rule5)) -> rule1))]
The cat is blue.
("cat" "is" "blue" "+")
triple1
The cat is kind.
("cat" "is" "kind" "+")
triple2
The cat is red.
("cat" "is" "red" "+")
triple3
The cat is rough.
("cat" "is" "rough" "+")
triple4
((triple5) -> (rule1 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
((((triple7) -> (rule4 % int2))) -> (rule1 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
((((triple8 triple11) -> (rule5 % int2))) -> (rule1 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat is young.
("cat" "is" "young" "+")
triple5
((triple7) -> (rule4 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
((triple8 triple11) -> (rule5 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
triple6
((triple8 triple12) -> (rule6 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cat sees the cow.
("cat" "sees" "cow" "+")
triple7
The cat visits the cow.
("cat" "visits" "cow" "+")
triple8
The cow is blue.
("cow" "is" "blue" "+")
triple9
The cow is kind.
("cow" "is" "kind" "+")
triple10
The cow likes the cat.
("cow" "likes" "cat" "+")
triple11
The cow visits the cat.
("cow" "visits" "cat" "+")
triple12
The cow visits the cow.
("cow" "visits" "cow" "+")
((triple11) -> (rule8 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow is young.
("cow" "is" "young" "+")
((((triple11) -> (rule8 % int2)) triple11) -> (rule5 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
((((((triple11) -> (rule8 % int3)) triple11) -> (rule5 % int2))) -> (rule1 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
int3