The cat sees the cow. The cow is red. The cow likes the cat. If someone sees the cat then the cat is round. If someone is round and they see the cow then they see the cat. If the cow likes the cat then the cow sees the cat.
The cat sees the cow.
("cat" "sees" "cow" "+")
The cow is red.
("cow" "is" "red" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
If someone sees the cat then the cat is round.
((("someone" "sees" "cat" "+")) -> ("cat" "is" "round" "+"))
If someone is round and they see the cow then they see the cat.
((("someone" "is" "round" "+") ("someone" "sees" "cow" "+")) -> ("someone" "sees" "cat" "+"))
If the cow likes the cat then the cow sees the cat.
((("cow" "likes" "cat" "+")) -> ("cow" "sees" "cat" "+"))
The cow is red.
True
1
proof
[(triple2)]
("cow" "is" "red" "+")
triple2
The cow does not like the cat.
False
1
inv-proof
[(triple3)]
("cow" "likes" "cat" "-")
triple3
The cow sees the cat.
True
2
proof
[(((triple3) -> rule3))]
("cow" "sees" "cat" "+")
((triple3) -> (rule3 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The cow does not see the cat.
False
2
inv-proof
[(((triple3) -> rule3))]
("cow" "sees" "cat" "-")
((triple3) -> (rule3 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The cat is round.
True
3
proof
[(((((triple3) -> rule3)) -> rule1))]
("cat" "is" "round" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cow sees the cat.
("cow" "sees" "cat" "+")
int2
The cat is not round.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule1))]
("cat" "is" "round" "-")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cow sees the cat.
("cow" "sees" "cat" "+")
int2
The cat sees the cat.
True
5
proof
[(((((((triple3) -> rule3)) -> rule1) triple1) -> rule2))]
("cat" "sees" "cat" "+")
((((((triple3) -> (rule3 % int3))) -> (rule1 % int2)) triple1) -> (rule2 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cow sees the cat.
("cow" "sees" "cat" "+")
int3
The cat does not see the cat.
False
5
inv-proof
[(((((((triple3) -> rule3)) -> rule1) triple1) -> rule2))]
("cat" "sees" "cat" "-")
((((((triple3) -> (rule3 % int3))) -> (rule1 % int2)) triple1) -> (rule2 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cow sees the cat.
("cow" "sees" "cat" "+")
int3
The cat is not cold.
Unknown
inv-random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "-")
The cat is young.
Unknown
random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "+")
The cow is not big.
Unknown
inv-random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "-")
The cat is big.
Unknown
random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "+")
The cow is not round.
Unknown
inv-random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "-")
The cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
@0: The cat sees the cow.[(triple1)] The cow is red.[(triple2)] The cow likes the cat.[(triple3)] @1: The cow sees the cat.[(((triple3) -> rule3))] @2: The cat is round.[(((((triple3) -> rule3)) -> rule1))] @3: The cat sees the cat.[(((((((triple3) -> rule3)) -> rule1) triple1) -> rule2))]
The cat sees the cow.
("cat" "sees" "cow" "+")
triple1
The cow is red.
("cow" "is" "red" "+")
triple2
The cow likes the cat.
("cow" "likes" "cat" "+")
triple3
The cow sees the cat.
("cow" "sees" "cat" "+")
((triple3) -> (rule3 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cow sees the cat.
("cow" "sees" "cat" "+")
int2
The cat sees the cat.
("cat" "sees" "cat" "+")
((((((triple3) -> (rule3 % int3))) -> (rule1 % int2)) triple1) -> (rule2 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cow sees the cat.
("cow" "sees" "cat" "+")
int3