The cat eats the cow. The cat is cold. The cat is rough. The cat likes the cow. The cat visits the cow. The cow eats the cat. The cow likes the cat. If the cat visits the cow and the cow likes the cat then the cat eats the cow. All cold people are nice. If someone is nice and they visit the cow then they are kind. If the cow visits the cat then the cat is rough. If someone visits the cat then the cat eats the cow. If someone is kind then they like the cat. If someone visits the cow and the cow eats the cat then they are rough. If the cat is kind then the cat likes the cow.
The cat eats the cow.
("cat" "eats" "cow" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat likes the cow.
("cat" "likes" "cow" "+")
The cat visits the cow.
("cat" "visits" "cow" "+")
The cow eats the cat.
("cow" "eats" "cat" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
If the cat visits the cow and the cow likes the cat then the cat eats the cow.
((("cat" "visits" "cow" "+") ("cow" "likes" "cat" "+")) -> ("cat" "eats" "cow" "+"))
All cold people are nice.
((("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
If someone is nice and they visit the cow then they are kind.
((("someone" "is" "nice" "+") ("someone" "visits" "cow" "+")) -> ("someone" "is" "kind" "+"))
If the cow visits the cat then the cat is rough.
((("cow" "visits" "cat" "+")) -> ("cat" "is" "rough" "+"))
If someone visits the cat then the cat eats the cow.
((("someone" "visits" "cat" "+")) -> ("cat" "eats" "cow" "+"))
If someone is kind then they like the cat.
((("someone" "is" "kind" "+")) -> ("someone" "likes" "cat" "+"))
If someone visits the cow and the cow eats the cat then they are rough.
((("someone" "visits" "cow" "+") ("cow" "eats" "cat" "+")) -> ("someone" "is" "rough" "+"))
If the cat is kind then the cat likes the cow.
((("cat" "is" "kind" "+")) -> ("cat" "likes" "cow" "+"))
The cat likes the cow.
True
1
proof
[(triple4 OR ((((((triple2) -> rule2) triple5) -> rule3)) -> rule8))]
("cat" "likes" "cow" "+")
triple4
((((((triple2) -> (rule2 % int3)) triple5) -> (rule3 % int2))) -> (rule8 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
The cat is not rough.
False
1
inv-proof
[(triple3 OR ((triple5 triple6) -> rule7))]
("cat" "is" "rough" "-")
triple3
((triple5 triple6) -> (rule7 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is nice.
True
2
proof
[(((triple2) -> rule2))]
("cat" "is" "nice" "+")
((triple2) -> (rule2 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is not nice.
False
2
inv-proof
[(((triple2) -> rule2))]
("cat" "is" "nice" "-")
((triple2) -> (rule2 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is kind.
True
4
proof
[(((((triple2) -> rule2) triple5) -> rule3))]
("cat" "is" "kind" "+")
((((triple2) -> (rule2 % int2)) triple5) -> (rule3 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is not kind.
False
4
inv-proof
[(((((triple2) -> rule2) triple5) -> rule3))]
("cat" "is" "kind" "-")
((((triple2) -> (rule2 % int2)) triple5) -> (rule3 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat likes the cat.
True
5
proof
[(((((((triple2) -> rule2) triple5) -> rule3)) -> rule6))]
("cat" "likes" "cat" "+")
((((((triple2) -> (rule2 % int3)) triple5) -> (rule3 % int2))) -> (rule6 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
The cat does not like the cat.
False
5
inv-proof
[(((((((triple2) -> rule2) triple5) -> rule3)) -> rule6))]
("cat" "likes" "cat" "-")
((((((triple2) -> (rule2 % int3)) triple5) -> (rule3 % int2))) -> (rule6 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
The cow is not nice.
Unknown
inv-rconc
[@1: The cow is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "nice" "-")
The cow is kind.
Unknown
rconc
[@1: The cow is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "is" "kind" "+")
The cow is not rough.
Unknown
inv-rconc
[@1: The cow is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cow" "is" "rough" "-")
The cow is red.
Unknown
random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "+")
The cat is not red.
Unknown
inv-random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "-")
The cow visits the cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "+")
The cow does not visit the cat.
Unknown
inv-random
[@0: The cow visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cat" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
@0: The cat eats the cow.[(triple1 OR ((triple5 triple7) -> rule1))] The cat is cold.[(triple2)] The cat is rough.[(triple3 OR ((triple5 triple6) -> rule7))] The cat likes the cow.[(triple4 OR ((((((triple2) -> rule2) triple5) -> rule3)) -> rule8))] The cat visits the cow.[(triple5)] The cow eats the cat.[(triple6)] The cow likes the cat.[(triple7)] @1: The cat is nice.[(((triple2) -> rule2))] @2: The cat is kind.[(((((triple2) -> rule2) triple5) -> rule3))] @3: The cat likes the cat.[(((((((triple2) -> rule2) triple5) -> rule3)) -> rule6))]
The cat eats the cow.
("cat" "eats" "cow" "+")
triple1
((triple5 triple7) -> (rule1 % int1))
The cat eats the cow.
("cat" "eats" "cow" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
triple2
The cat is rough.
("cat" "is" "rough" "+")
triple3
((triple5 triple6) -> (rule7 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
triple4
((((((triple2) -> (rule2 % int3)) triple5) -> (rule3 % int2))) -> (rule8 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
The cat visits the cow.
("cat" "visits" "cow" "+")
triple5
The cow eats the cat.
("cow" "eats" "cat" "+")
triple6
The cow likes the cat.
("cow" "likes" "cat" "+")
triple7
The cat is nice.
("cat" "is" "nice" "+")
((triple2) -> (rule2 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
((((triple2) -> (rule2 % int2)) triple5) -> (rule3 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat likes the cat.
("cat" "likes" "cat" "+")
((((((triple2) -> (rule2 % int3)) triple5) -> (rule3 % int2))) -> (rule6 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3