The cat chases the cow. The cat is not nice. The cat is red. The cat sees the cow. The cat visits the cow. The cow chases the cat. The cow is big. The cow is green. The cow is kind. The cow visits the cat. If something chases the cow then the cow visits the cat. If something chases the cat and the cat does not see the cow then the cow does not visit the cat. If something visits the cow and it does not see the cow then the cow visits the cat. If something chases the cow then the cow sees the cat. If the cow sees the cat and the cat is red then the cow chases the cat. If something sees the cat then it chases the cow.
The cat chases the cow.
("cat" "chases" "cow" "+")
The cat is not nice.
("cat" "is" "nice" "-")
The cat is red.
("cat" "is" "red" "+")
The cat sees the cow.
("cat" "sees" "cow" "+")
The cat visits the cow.
("cat" "visits" "cow" "+")
The cow chases the cat.
("cow" "chases" "cat" "+")
The cow is big.
("cow" "is" "big" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
If something chases the cow then the cow visits the cat.
((("something" "chases" "cow" "+")) -> ("cow" "visits" "cat" "+"))
If something chases the cat and the cat does not see the cow then the cow does not visit the cat.
((("something" "chases" "cat" "+") ("cat" "sees" "cow" "~")) -> ("cow" "visits" "cat" "-"))
If something visits the cow and it does not see the cow then the cow visits the cat.
((("something" "visits" "cow" "+") ("something" "sees" "cow" "~")) -> ("cow" "visits" "cat" "+"))
If something chases the cow then the cow sees the cat.
((("something" "chases" "cow" "+")) -> ("cow" "sees" "cat" "+"))
If the cow sees the cat and the cat is red then the cow chases the cat.
((("cow" "sees" "cat" "+") ("cat" "is" "red" "+")) -> ("cow" "chases" "cat" "+"))
If something sees the cat then it chases the cow.
((("something" "sees" "cat" "+")) -> ("something" "chases" "cow" "+"))
The cat is red.
True
1
proof
[(triple3)]
("cat" "is" "red" "+")
triple3
The cat does not visit the cow.
False
1
inv-proof
[(triple5)]
("cat" "visits" "cow" "-")
triple5
The cow sees the cat.
True
2
proof
[(((triple1) -> rule4))]
("cow" "sees" "cat" "+")
((triple1) -> (rule4 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The cow does not see the cat.
False
2
inv-proof
[(((triple1) -> rule4))]
("cow" "sees" "cat" "-")
((triple1) -> (rule4 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The cow chases the cow.
True
3
proof
[(((((triple1) -> rule4)) -> rule6))]
("cow" "chases" "cow" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow sees the cat.
("cow" "sees" "cat" "+")
int2
The cow does not chase the cow.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule6))]
("cow" "chases" "cow" "-")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow sees the cat.
("cow" "sees" "cat" "+")
int2
The cat is not big.
Unknown
inv-random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The cow is red.
Unknown
random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "+")
The cat does not chase the cat.
Unknown
inv-random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "-")
The cat is green.
Unknown
random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "+")
@0: The cat chases the cow.[(triple1)] The cat is not nice.[(triple2)] The cat is red.[(triple3)] The cat sees the cow.[(triple4)] The cat visits the cow.[(triple5)] The cow chases the cat.[(triple6 OR ((((triple1) -> rule4) triple3) -> rule5))] The cow is big.[(triple7)] The cow is green.[(triple8)] The cow is kind.[(triple9)] The cow visits the cat.[(triple10 OR ((triple1) -> rule1) OR ((((((triple1) -> rule4)) -> rule6)) -> rule1))] @1: The cow sees the cat.[(((triple1) -> rule4))] @2: The cow chases the cow.[(((((triple1) -> rule4)) -> rule6))]
The cat chases the cow.
("cat" "chases" "cow" "+")
triple1
The cat is not nice.
("cat" "is" "nice" "-")
triple2
The cat is red.
("cat" "is" "red" "+")
triple3
The cat sees the cow.
("cat" "sees" "cow" "+")
triple4
The cat visits the cow.
("cat" "visits" "cow" "+")
triple5
The cow chases the cat.
("cow" "chases" "cat" "+")
triple6
((((triple1) -> (rule4 % int2)) triple3) -> (rule5 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cow sees the cat.
("cow" "sees" "cat" "+")
int2
The cow is big.
("cow" "is" "big" "+")
triple7
The cow is green.
("cow" "is" "green" "+")
triple8
The cow is kind.
("cow" "is" "kind" "+")
triple9
The cow visits the cat.
("cow" "visits" "cat" "+")
triple10
((triple1) -> (rule1 % int1))
The cow visits the cat.
("cow" "visits" "cat" "+")
int1
((((((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The cow visits the cat.
("cow" "visits" "cat" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow sees the cat.
("cow" "sees" "cat" "+")
int3
The cow sees the cat.
("cow" "sees" "cat" "+")
((triple1) -> (rule4 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow sees the cat.
("cow" "sees" "cat" "+")
int2