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