The cat does not chase the cow. The cow chases the cat. The cow likes the cat. If someone is rough and they visit the cow then the cow chases the cat. If someone likes the cow then the cow chases the cat. If someone is red then they do not chase the cow. If someone visits the cat and they do not like the cat then they are rough. If the cat likes the cow and the cow likes the cat then the cow visits the cat. If someone likes the cat then the cat likes the cow. If the cow visits the cat then the cow is not cold. If someone visits the cat and the cat likes the cow then the cow is round.
The cat does not chase the cow.
("cat" "chases" "cow" "-")
The cow chases the cat.
("cow" "chases" "cat" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
If someone is rough and they visit the cow then the cow chases the cat.
((("someone" "is" "rough" "+") ("someone" "visits" "cow" "+")) -> ("cow" "chases" "cat" "+"))
If someone likes the cow then the cow chases the cat.
((("someone" "likes" "cow" "+")) -> ("cow" "chases" "cat" "+"))
If someone is red then they do not chase the cow.
((("someone" "is" "red" "+")) -> ("someone" "chases" "cow" "-"))
If someone visits the cat and they do not like the cat then they are rough.
((("someone" "visits" "cat" "+") ("someone" "likes" "cat" "~")) -> ("someone" "is" "rough" "+"))
If the cat likes the cow and the cow likes the cat then the cow visits the cat.
((("cat" "likes" "cow" "+") ("cow" "likes" "cat" "+")) -> ("cow" "visits" "cat" "+"))
If someone likes the cat then the cat likes the cow.
((("someone" "likes" "cat" "+")) -> ("cat" "likes" "cow" "+"))
If the cow visits the cat then the cow is not cold.
((("cow" "visits" "cat" "+")) -> ("cow" "is" "cold" "-"))
If someone visits the cat and the cat likes the cow then the cow is round.
((("someone" "visits" "cat" "+") ("cat" "likes" "cow" "+")) -> ("cow" "is" "round" "+"))
The cow chases the cat.
True
1
proof
[(triple2 OR ((((triple3) -> rule6)) -> rule2))]
("cow" "chases" "cat" "+")
triple2
((((triple3) -> (rule6 % int2))) -> (rule2 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
int2
The cow does not like the cat.
False
1
inv-proof
[(triple3)]
("cow" "likes" "cat" "-")
triple3
The cat likes the cow.
True
2
proof
[(((triple3) -> rule6))]
("cat" "likes" "cow" "+")
((triple3) -> (rule6 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cat does not like the cow.
False
2
inv-proof
[(((triple3) -> rule6))]
("cat" "likes" "cow" "-")
((triple3) -> (rule6 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cow visits the cat.
True
4
proof
[(((((triple3) -> rule6) triple3) -> rule5))]
("cow" "visits" "cat" "+")
((((triple3) -> (rule6 % int2)) triple3) -> (rule5 % int1))
The cow visits the cat.
("cow" "visits" "cat" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
int2
The cow does not visit the cat.
False
4
inv-proof
[(((((triple3) -> rule6) triple3) -> rule5))]
("cow" "visits" "cat" "-")
((((triple3) -> (rule6 % int2)) triple3) -> (rule5 % int1))
The cow visits the cat.
("cow" "visits" "cat" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
int2
The cow is not cold.
True
5
proof
[(((((((triple3) -> rule6) triple3) -> rule5)) -> rule7))]
("cow" "is" "cold" "-")
((((((triple3) -> (rule6 % int3)) triple3) -> (rule5 % int2))) -> (rule7 % int1))
The cow is not cold.
("cow" "is" "cold" "-")
int1
The cow visits the cat.
("cow" "visits" "cat" "+")
int2
The cat likes the cow.
("cat" "likes" "cow" "+")
int3
The cow is cold.
False
5
inv-proof
[(((((((triple3) -> rule6) triple3) -> rule5)) -> rule7))]
("cow" "is" "cold" "+")
((((((triple3) -> (rule6 % int3)) triple3) -> (rule5 % int2))) -> (rule7 % int1))
The cow is not cold.
("cow" "is" "cold" "-")
int1
The cow visits the cat.
("cow" "visits" "cat" "+")
int2
The cat likes the cow.
("cat" "likes" "cow" "+")
int3
The cow is not rough.
Unknown
inv-rconc
[@1: The cow is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "is" "rough" "-")
The cat is rough.
Unknown
rconc
[@1: The cat is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "is" "rough" "+")
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The cat is cold.
Unknown
random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "+")
The cow does not like the cow.
Unknown
inv-random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "-")
The cat is green.
Unknown
random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "+")
The cat does not chase the cat.
Unknown
inv-random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "-")
The cat is red.
Unknown
random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "+")
@0: The cat does not chase the cow.[(triple1)] The cow chases the cat.[(triple2 OR ((((triple3) -> rule6)) -> rule2))] The cow likes the cat.[(triple3)] @1: The cat likes the cow.[(((triple3) -> rule6))] @2: The cow visits the cat.[(((((triple3) -> rule6) triple3) -> rule5))] @3: The cow is not cold.[(((((((triple3) -> rule6) triple3) -> rule5)) -> rule7))] The cow is round.[(((((((triple3) -> rule6) triple3) -> rule5) ((triple3) -> rule6)) -> rule8))]
The cat does not chase the cow.
("cat" "chases" "cow" "-")
triple1
The cow chases the cat.
("cow" "chases" "cat" "+")
triple2
((((triple3) -> (rule6 % int2))) -> (rule2 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
int2
The cow likes the cat.
("cow" "likes" "cat" "+")
triple3
The cat likes the cow.
("cat" "likes" "cow" "+")
((triple3) -> (rule6 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cow visits the cat.
("cow" "visits" "cat" "+")
((((triple3) -> (rule6 % int2)) triple3) -> (rule5 % int1))
The cow visits the cat.
("cow" "visits" "cat" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
int2
The cow is not cold.
("cow" "is" "cold" "-")
((((((triple3) -> (rule6 % int3)) triple3) -> (rule5 % int2))) -> (rule7 % int1))
The cow is not cold.
("cow" "is" "cold" "-")
int1
The cow visits the cat.
("cow" "visits" "cat" "+")
int2
The cat likes the cow.
("cat" "likes" "cow" "+")
int3
The cow is round.
("cow" "is" "round" "+")
((((((triple3) -> (rule6 % int3)) triple3) -> (rule5 % int2)) ((triple3) -> (rule6 % int3))) -> (rule8 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow visits the cat.
("cow" "visits" "cat" "+")
int2
The cat likes the cow.
("cat" "likes" "cow" "+")
int3