The cat is young. The cat needs the cow. The cow is big. The cow is nice. The cow needs the cat. The cow sees the cat. The cow visits the cat. If something is nice and it sees the cat then the cat visits the cow.
The cat is young.
("cat" "is" "young" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cow is big.
("cow" "is" "big" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
If something is nice and it sees the cat then the cat visits the cow.
((("something" "is" "nice" "+") ("something" "sees" "cat" "+")) -> ("cat" "visits" "cow" "+"))
The cow is nice.
True
1
proof
[(triple4)]
("cow" "is" "nice" "+")
triple4
The cow is not nice.
False
1
inv-proof
[(triple4)]
("cow" "is" "nice" "-")
triple4
The cat visits the cow.
True
3
proof
[(((triple4 triple6) -> rule1))]
("cat" "visits" "cow" "+")
((triple4 triple6) -> (rule1 % int1))
The cat visits the cow.
("cat" "visits" "cow" "+")
int1
The cat does not visit the cow.
False
3
inv-proof
[(((triple4 triple6) -> rule1))]
("cat" "visits" "cow" "-")
((triple4 triple6) -> (rule1 % int1))
The cat visits the cow.
("cat" "visits" "cow" "+")
int1
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The cat is big.
Unknown
random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "+")
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 needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
@0: The cat is young.[(triple1)] The cat needs the cow.[(triple2)] The cow is big.[(triple3)] The cow is nice.[(triple4)] The cow needs the cat.[(triple5)] The cow sees the cat.[(triple6)] The cow visits the cat.[(triple7)] @1: The cat visits the cow.[(((triple4 triple6) -> rule1))]
The cat is young.
("cat" "is" "young" "+")
triple1
The cat needs the cow.
("cat" "needs" "cow" "+")
triple2
The cow is big.
("cow" "is" "big" "+")
triple3
The cow is nice.
("cow" "is" "nice" "+")
triple4
The cow needs the cat.
("cow" "needs" "cat" "+")
triple5
The cow sees the cat.
("cow" "sees" "cat" "+")
triple6
The cow visits the cat.
("cow" "visits" "cat" "+")
triple7
The cat visits the cow.
("cat" "visits" "cow" "+")
((triple4 triple6) -> (rule1 % int1))
The cat visits the cow.
("cat" "visits" "cow" "+")
int1