The cat is young. The cat likes the cow. The cat needs the cow. The cow is kind. The cow is young. The cow needs the cat. The cow sees the cat. If something sees the cow and the cow does not need the cat then the cow is rough. If the cat sees the cow then the cow likes the cat. If something is young then it sees the cow. If something sees the cat and it likes the cat then it is not round. If the cow likes the cat then the cat likes the cow. If the cat is young then the cat needs the cow.
The cat is young.
("cat" "is" "young" "+")
The cat likes the cow.
("cat" "likes" "cow" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is young.
("cow" "is" "young" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
If something sees the cow and the cow does not need the cat then the cow is rough.
((("something" "sees" "cow" "+") ("cow" "needs" "cat" "~")) -> ("cow" "is" "rough" "+"))
If the cat sees the cow then the cow likes the cat.
((("cat" "sees" "cow" "+")) -> ("cow" "likes" "cat" "+"))
If something is young then it sees the cow.
((("something" "is" "young" "+")) -> ("something" "sees" "cow" "+"))
If something sees the cat and it likes the cat then it is not round.
((("something" "sees" "cat" "+") ("something" "likes" "cat" "+")) -> ("something" "is" "round" "-"))
If the cow likes the cat then the cat likes the cow.
((("cow" "likes" "cat" "+")) -> ("cat" "likes" "cow" "+"))
If the cat is young then the cat needs the cow.
((("cat" "is" "young" "+")) -> ("cat" "needs" "cow" "+"))
The cow needs the cat.
True
1
proof
[(triple6)]
("cow" "needs" "cat" "+")
triple6
The cow does not need the cat.
False
1
inv-proof
[(triple6)]
("cow" "needs" "cat" "-")
triple6
The cat sees the cow.
True
2
proof
[(((triple1) -> rule3))]
("cat" "sees" "cow" "+")
((triple1) -> (rule3 % int1))
The cat sees the cow.
("cat" "sees" "cow" "+")
int1
The cow does not see the cow.
False
2
inv-proof
[(((triple5) -> rule3))]
("cow" "sees" "cow" "-")
((triple5) -> (rule3 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow likes the cat.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("cow" "likes" "cat" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The cow likes the cat.
("cow" "likes" "cat" "+")
int1
The cat sees the cow.
("cat" "sees" "cow" "+")
int2
The cow does not like the cat.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("cow" "likes" "cat" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The cow likes the cat.
("cow" "likes" "cat" "+")
int1
The cat sees the cow.
("cat" "sees" "cow" "+")
int2
The cow is not round.
True
5
proof
[(((triple7 ((((triple1) -> rule3)) -> rule2)) -> rule4))]
("cow" "is" "round" "-")
((triple7 ((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cow is not round.
("cow" "is" "round" "-")
int1
The cow likes the cat.
("cow" "likes" "cat" "+")
int2
The cat sees the cow.
("cat" "sees" "cow" "+")
int3
The cow is round.
False
5
inv-proof
[(((triple7 ((((triple1) -> rule3)) -> rule2)) -> rule4))]
("cow" "is" "round" "+")
((triple7 ((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cow is not round.
("cow" "is" "round" "-")
int1
The cow likes the cat.
("cow" "likes" "cat" "+")
int2
The cat sees the cow.
("cat" "sees" "cow" "+")
int3
The cow is not rough.
Unknown
inv-rconc
[@1: The cow is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "is" "rough" "-")
The cow is nice.
Unknown
random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "+")
The cat is not rough.
Unknown
inv-random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "-")
The cat is round.
Unknown
random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "+")
The cat is not nice.
Unknown
inv-random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
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 kind.
Unknown
random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "+")
@0: The cat is young.[(triple1)] The cat likes the cow.[(triple2 OR ((((((triple1) -> rule3)) -> rule2)) -> rule5))] The cat needs the cow.[(triple3 OR ((triple1) -> rule6))] The cow is kind.[(triple4)] The cow is young.[(triple5)] The cow needs the cat.[(triple6)] The cow sees the cat.[(triple7)] @1: The cat sees the cow.[(((triple1) -> rule3))] The cow sees the cow.[(((triple5) -> rule3))] @2: The cow likes the cat.[(((((triple1) -> rule3)) -> rule2))] @3: The cow is not round.[(((triple7 ((((triple1) -> rule3)) -> rule2)) -> rule4))]
The cat is young.
("cat" "is" "young" "+")
triple1
The cat likes the cow.
("cat" "likes" "cow" "+")
triple2
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cow likes the cat.
("cow" "likes" "cat" "+")
int2
The cat sees the cow.
("cat" "sees" "cow" "+")
int3
The cat needs the cow.
("cat" "needs" "cow" "+")
triple3
((triple1) -> (rule6 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
triple4
The cow is young.
("cow" "is" "young" "+")
triple5
The cow needs the cat.
("cow" "needs" "cat" "+")
triple6
The cow sees the cat.
("cow" "sees" "cat" "+")
triple7
The cat sees the cow.
("cat" "sees" "cow" "+")
((triple1) -> (rule3 % int1))
The cat sees the cow.
("cat" "sees" "cow" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
((triple5) -> (rule3 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow likes the cat.
("cow" "likes" "cat" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The cow likes the cat.
("cow" "likes" "cat" "+")
int1
The cat sees the cow.
("cat" "sees" "cow" "+")
int2
The cow is not round.
("cow" "is" "round" "-")
((triple7 ((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cow is not round.
("cow" "is" "round" "-")
int1
The cow likes the cat.
("cow" "likes" "cat" "+")
int2
The cat sees the cow.
("cat" "sees" "cow" "+")
int3