The cat chases the cow. The cat is cold. The cat is round. The cat needs the cow. The cat sees the cow. The cow needs the cat. The cow sees the cat. If something sees the cat and it needs the cat then the cat chases the cow. If something chases the cow and the cow sees the cat then the cow is round.
The cat chases the cow.
("cat" "chases" "cow" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is round.
("cat" "is" "round" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cat sees the cow.
("cat" "sees" "cow" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
If something sees the cat and it needs the cat then the cat chases the cow.
((("something" "sees" "cat" "+") ("something" "needs" "cat" "+")) -> ("cat" "chases" "cow" "+"))
If something chases the cow and the cow sees the cat then the cow is round.
((("something" "chases" "cow" "+") ("cow" "sees" "cat" "+")) -> ("cow" "is" "round" "+"))
The cat sees the cow.
True
1
proof
[(triple5)]
("cat" "sees" "cow" "+")
triple5
The cat does not chase the cow.
False
1
inv-proof
[(triple1 OR ((triple7 triple6) -> rule1))]
("cat" "chases" "cow" "-")
triple1
((triple7 triple6) -> (rule1 % int1))
The cat chases the cow.
("cat" "chases" "cow" "+")
int1
The cow is round.
True
3
proof
[(((triple1 triple7) -> rule2) OR ((((triple7 triple6) -> rule1) triple7) -> rule2))]
("cow" "is" "round" "+")
((triple1 triple7) -> (rule2 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
((((triple7 triple6) -> (rule1 % int2)) triple7) -> (rule2 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cat chases the cow.
("cat" "chases" "cow" "+")
int2
The cow is not round.
False
3
inv-proof
[(((triple1 triple7) -> rule2) OR ((((triple7 triple6) -> rule1) triple7) -> rule2))]
("cow" "is" "round" "-")
((triple1 triple7) -> (rule2 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
((((triple7 triple6) -> (rule1 % int2)) triple7) -> (rule2 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cat chases the cow.
("cat" "chases" "cow" "+")
int2
The cat is not nice.
Unknown
inv-random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "-")
The cat is kind.
Unknown
random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "+")
The cow is not cold.
Unknown
inv-random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "-")
The cow is rough.
Unknown
random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "+")
@0: The cat chases the cow.[(triple1 OR ((triple7 triple6) -> rule1))] The cat is cold.[(triple2)] The cat is round.[(triple3)] The cat needs the cow.[(triple4)] The cat sees the cow.[(triple5)] The cow needs the cat.[(triple6)] The cow sees the cat.[(triple7)] @1: The cow is round.[(((triple1 triple7) -> rule2) OR ((((triple7 triple6) -> rule1) triple7) -> rule2))]
The cat chases the cow.
("cat" "chases" "cow" "+")
triple1
((triple7 triple6) -> (rule1 % int1))
The cat chases the cow.
("cat" "chases" "cow" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
triple2
The cat is round.
("cat" "is" "round" "+")
triple3
The cat needs the cow.
("cat" "needs" "cow" "+")
triple4
The cat sees the cow.
("cat" "sees" "cow" "+")
triple5
The cow needs the cat.
("cow" "needs" "cat" "+")
triple6
The cow sees the cat.
("cow" "sees" "cat" "+")
triple7
The cow is round.
("cow" "is" "round" "+")
((triple1 triple7) -> (rule2 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
((((triple7 triple6) -> (rule1 % int2)) triple7) -> (rule2 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cat chases the cow.
("cat" "chases" "cow" "+")
int2