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