The cat sees the cow. The cow does not chase the cat. If someone needs the cat and they see the cat then the cat is not round. If the cat chases the cow and the cow does not chase the cat then the cow is rough. If the cat sees the cow and the cat needs the cow then the cow is round. If someone needs the cat then the cat needs the cow. If someone sees the cow then they need the cat. If someone chases the cow and the cow chases the cat then they need the cat.
The cat sees the cow.
("cat" "sees" "cow" "+")
The cow does not chase the cat.
("cow" "chases" "cat" "-")
If someone needs the cat and they see the cat then the cat is not round.
((("someone" "needs" "cat" "+") ("someone" "sees" "cat" "+")) -> ("cat" "is" "round" "-"))
If the cat chases the cow and the cow does not chase the cat then the cow is rough.
((("cat" "chases" "cow" "+") ("cow" "chases" "cat" "~")) -> ("cow" "is" "rough" "+"))
If the cat sees the cow and the cat needs the cow then the cow is round.
((("cat" "sees" "cow" "+") ("cat" "needs" "cow" "+")) -> ("cow" "is" "round" "+"))
If someone needs the cat then the cat needs the cow.
((("someone" "needs" "cat" "+")) -> ("cat" "needs" "cow" "+"))
If someone sees the cow then they need the cat.
((("someone" "sees" "cow" "+")) -> ("someone" "needs" "cat" "+"))
If someone chases the cow and the cow chases the cat then they need the cat.
((("someone" "chases" "cow" "+") ("cow" "chases" "cat" "+")) -> ("someone" "needs" "cat" "+"))
The cow does not chase the cat.
True
1
proof
[(triple2)]
("cow" "chases" "cat" "-")
triple2
The cow chases the cat.
False
1
inv-proof
[(triple2)]
("cow" "chases" "cat" "+")
triple2
The cat needs the cat.
True
2
proof
[(((triple1) -> rule5))]
("cat" "needs" "cat" "+")
((triple1) -> (rule5 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat does not need the cat.
False
2
inv-proof
[(((triple1) -> rule5))]
("cat" "needs" "cat" "-")
((triple1) -> (rule5 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat needs the cow.
True
3
proof
[(((((triple1) -> rule5)) -> rule4))]
("cat" "needs" "cow" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The cat does not need the cow.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule4))]
("cat" "needs" "cow" "-")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The cow does not need the cat.
Unknown
inv-rconc
[@1: The cow needs the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "needs" "cat" "-")
The cow is rough.
Unknown
rconc
[@1: The cow is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "rough" "+")
The cow does not need the cow.
Unknown
inv-random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "-")
The cat is blue.
Unknown
random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "+")
The cat is not green.
Unknown
inv-random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
@0: The cat sees the cow.[(triple1)] The cow does not chase the cat.[(triple2)] @1: The cat needs the cat.[(((triple1) -> rule5))] @2: The cat needs the cow.[(((((triple1) -> rule5)) -> rule4))] @3: The cow is round.[(((triple1 ((((triple1) -> rule5)) -> rule4)) -> rule3))]
The cat sees the cow.
("cat" "sees" "cow" "+")
triple1
The cow does not chase the cat.
("cow" "chases" "cat" "-")
triple2
The cat needs the cat.
("cat" "needs" "cat" "+")
((triple1) -> (rule5 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat needs the cow.
("cat" "needs" "cow" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The cow is round.
("cow" "is" "round" "+")
((triple1 ((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cat needs the cow.
("cat" "needs" "cow" "+")
int2
The cat needs the cat.
("cat" "needs" "cat" "+")
int3