The cat does not chase the cow. The cat eats the cow. The cat is cold. The cat is kind. The cat is red. The cow eats the cat. The cow is kind. The cow is not red. The cow is not round. The cow sees the cat. If something chases the cow then the cow eats the cat. If something chases the cat then the cat is not big. If the cat is big and the cat does not eat the cow then the cat chases the cow. If the cat eats the cow then the cat sees the cow. If something sees the cow then it sees the cat. If something sees the cat and it eats the cat then it is kind. If something is cold and it sees the cat then it eats the cat. If something is big and it does not see the cat then it is round.
The cat does not chase the cow.
("cat" "chases" "cow" "-")
The cat eats the cow.
("cat" "eats" "cow" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is red.
("cat" "is" "red" "+")
The cow eats the cat.
("cow" "eats" "cat" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is not red.
("cow" "is" "red" "-")
The cow is not round.
("cow" "is" "round" "-")
The cow sees the cat.
("cow" "sees" "cat" "+")
If something chases the cow then the cow eats the cat.
((("something" "chases" "cow" "+")) -> ("cow" "eats" "cat" "+"))
If something chases the cat then the cat is not big.
((("something" "chases" "cat" "+")) -> ("cat" "is" "big" "-"))
If the cat is big and the cat does not eat the cow then the cat chases the cow.
((("cat" "is" "big" "+") ("cat" "eats" "cow" "~")) -> ("cat" "chases" "cow" "+"))
If the cat eats the cow then the cat sees the cow.
((("cat" "eats" "cow" "+")) -> ("cat" "sees" "cow" "+"))
If something sees the cow then it sees the cat.
((("something" "sees" "cow" "+")) -> ("something" "sees" "cat" "+"))
If something sees the cat and it eats the cat then it is kind.
((("something" "sees" "cat" "+") ("something" "eats" "cat" "+")) -> ("something" "is" "kind" "+"))
If something is cold and it sees the cat then it eats the cat.
((("something" "is" "cold" "+") ("something" "sees" "cat" "+")) -> ("something" "eats" "cat" "+"))
If something is big and it does not see the cat then it is round.
((("something" "is" "big" "+") ("something" "sees" "cat" "~")) -> ("something" "is" "round" "+"))
The cow is kind.
True
1
proof
[(triple7 OR ((triple10 triple6) -> rule6))]
("cow" "is" "kind" "+")
triple7
((triple10 triple6) -> (rule6 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cat is not red.
False
1
inv-proof
[(triple5)]
("cat" "is" "red" "-")
triple5
The cat sees the cow.
True
2
proof
[(((triple2) -> rule4))]
("cat" "sees" "cow" "+")
((triple2) -> (rule4 % int1))
The cat sees the cow.
("cat" "sees" "cow" "+")
int1
The cat does not see the cow.
False
2
inv-proof
[(((triple2) -> rule4))]
("cat" "sees" "cow" "-")
((triple2) -> (rule4 % int1))
The cat sees the cow.
("cat" "sees" "cow" "+")
int1
The cat sees the cat.
True
3
proof
[(((((triple2) -> rule4)) -> rule5))]
("cat" "sees" "cat" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat sees the cow.
("cat" "sees" "cow" "+")
int2
The cat does not see the cat.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule5))]
("cat" "sees" "cat" "-")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat sees the cow.
("cat" "sees" "cow" "+")
int2
The cat eats the cat.
True
5
proof
[(((triple3 ((((triple2) -> rule4)) -> rule5)) -> rule7))]
("cat" "eats" "cat" "+")
((triple3 ((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The cat sees the cow.
("cat" "sees" "cow" "+")
int3
The cat does not eat the cat.
False
5
inv-proof
[(((triple3 ((((triple2) -> rule4)) -> rule5)) -> rule7))]
("cat" "eats" "cat" "-")
((triple3 ((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The cat sees the cow.
("cat" "sees" "cow" "+")
int3
The cat is not round.
Unknown
inv-rconc
[@1: The cat is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cat" "is" "round" "-")
The cat is big.
Unknown
random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "+")
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
The cow is not big.
Unknown
inv-random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "-")
The cow chases the cat.
Unknown
random
[@0: The cow chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cat" "+")
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 cow is cold.
Unknown
random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "+")
@0: The cat does not chase the cow.[(triple1)] The cat eats the cow.[(triple2)] The cat is cold.[(triple3)] The cat is kind.[(triple4 OR ((((((triple2) -> rule4)) -> rule5) ((triple3 ((((triple2) -> rule4)) -> rule5)) -> rule7)) -> rule6))] The cat is red.[(triple5)] The cow eats the cat.[(triple6)] The cow is kind.[(triple7 OR ((triple10 triple6) -> rule6))] The cow is not red.[(triple8)] The cow is not round.[(triple9)] The cow sees the cat.[(triple10)] @1: The cat sees the cow.[(((triple2) -> rule4))] @2: The cat sees the cat.[(((((triple2) -> rule4)) -> rule5))] @3: The cat eats the cat.[(((triple3 ((((triple2) -> rule4)) -> rule5)) -> rule7))]
The cat does not chase the cow.
("cat" "chases" "cow" "-")
triple1
The cat eats the cow.
("cat" "eats" "cow" "+")
triple2
The cat is cold.
("cat" "is" "cold" "+")
triple3
The cat is kind.
("cat" "is" "kind" "+")
triple4
((((((triple2) -> (rule4 % int4))) -> (rule5 % int3)) ((triple3 ((((triple2) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
int2
The cat sees the cat.
("cat" "sees" "cat" "+")
int3
The cat sees the cow.
("cat" "sees" "cow" "+")
int4
The cat is red.
("cat" "is" "red" "+")
triple5
The cow eats the cat.
("cow" "eats" "cat" "+")
triple6
The cow is kind.
("cow" "is" "kind" "+")
triple7
((triple10 triple6) -> (rule6 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is not red.
("cow" "is" "red" "-")
triple8
The cow is not round.
("cow" "is" "round" "-")
triple9
The cow sees the cat.
("cow" "sees" "cat" "+")
triple10
The cat sees the cow.
("cat" "sees" "cow" "+")
((triple2) -> (rule4 % int1))
The cat sees the cow.
("cat" "sees" "cow" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat sees the cow.
("cat" "sees" "cow" "+")
int2
The cat eats the cat.
("cat" "eats" "cat" "+")
((triple3 ((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The cat sees the cow.
("cat" "sees" "cow" "+")
int3