The cat is round. The cow is green. If someone is round then they chase the cow. If someone is red then they do not chase the cow. If the cat chases the cow then the cat is young. If someone is young then they chase the cat. If someone sees the cat and they do not chase the cow then the cow chases the cat. If someone chases the cat and the cat chases the cow then the cat does not eat the cow.
The cat is round.
("cat" "is" "round" "+")
The cow is green.
("cow" "is" "green" "+")
If someone is round then they chase the cow.
((("someone" "is" "round" "+")) -> ("someone" "chases" "cow" "+"))
If someone is red then they do not chase the cow.
((("someone" "is" "red" "+")) -> ("someone" "chases" "cow" "-"))
If the cat chases the cow then the cat is young.
((("cat" "chases" "cow" "+")) -> ("cat" "is" "young" "+"))
If someone is young then they chase the cat.
((("someone" "is" "young" "+")) -> ("someone" "chases" "cat" "+"))
If someone sees the cat and they do not chase the cow then the cow chases the cat.
((("someone" "sees" "cat" "+") ("someone" "chases" "cow" "~")) -> ("cow" "chases" "cat" "+"))
If someone chases the cat and the cat chases the cow then the cat does not eat the cow.
((("someone" "chases" "cat" "+") ("cat" "chases" "cow" "+")) -> ("cat" "eats" "cow" "-"))
The cat is round.
True
1
proof
[(triple1)]
("cat" "is" "round" "+")
triple1
The cow is not green.
False
1
inv-proof
[(triple2)]
("cow" "is" "green" "-")
triple2
The cat chases the cow.
True
2
proof
[(((triple1) -> rule1))]
("cat" "chases" "cow" "+")
((triple1) -> (rule1 % int1))
The cat chases the cow.
("cat" "chases" "cow" "+")
int1
The cat does not chase the cow.
False
2
inv-proof
[(((triple1) -> rule1))]
("cat" "chases" "cow" "-")
((triple1) -> (rule1 % int1))
The cat chases the cow.
("cat" "chases" "cow" "+")
int1
The cat is young.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("cat" "is" "young" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat chases the cow.
("cat" "chases" "cow" "+")
int2
The cat is not young.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("cat" "is" "young" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat chases the cow.
("cat" "chases" "cow" "+")
int2
The cat chases the cat.
True
4
proof
[(((((((triple1) -> rule1)) -> rule3)) -> rule4))]
("cat" "chases" "cat" "+")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat chases the cow.
("cat" "chases" "cow" "+")
int3
The cat does not chase the cat.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule3)) -> rule4))]
("cat" "chases" "cat" "-")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat chases the cow.
("cat" "chases" "cow" "+")
int3
The cow does not chase the cat.
Unknown
inv-rconc
[@1: The cow chases the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "chases" "cat" "-")
The cow chases the cow.
Unknown
rconc
[@1: The cow chases the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "chases" "cow" "+")
The cat is not nice.
Unknown
inv-random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
The cat is not green.
Unknown
inv-random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "-")
The cow sees the cat.
Unknown
random
[@0: The cow sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cat" "+")
The cow is not red.
Unknown
inv-random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
@0: The cat is round.[(triple1)] The cow is green.[(triple2)] @1: The cat chases the cow.[(((triple1) -> rule1))] @2: The cat is young.[(((((triple1) -> rule1)) -> rule3))] @3: The cat chases the cat.[(((((((triple1) -> rule1)) -> rule3)) -> rule4))] @4: The cat does not eat the cow.[(((((((((triple1) -> rule1)) -> rule3)) -> rule4) ((triple1) -> rule1)) -> rule6))]
The cat is round.
("cat" "is" "round" "+")
triple1
The cow is green.
("cow" "is" "green" "+")
triple2
The cat chases the cow.
("cat" "chases" "cow" "+")
((triple1) -> (rule1 % int1))
The cat chases the cow.
("cat" "chases" "cow" "+")
int1
The cat is young.
("cat" "is" "young" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat chases the cow.
("cat" "chases" "cow" "+")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat chases the cow.
("cat" "chases" "cow" "+")
int3
The cat does not eat the cow.
("cat" "eats" "cow" "-")
((((((((triple1) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule4 % int2)) ((triple1) -> (rule1 % int4))) -> (rule6 % int1))
The cat does not eat the cow.
("cat" "eats" "cow" "-")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The cat is young.
("cat" "is" "young" "+")
int3
The cat chases the cow.
("cat" "chases" "cow" "+")
int4