The cat eats the cow. The cat eats the rabbit. The cat eats the tiger. The cat is young. The cat needs the cow. The cat needs the tiger. The cow eats the cat. The cow eats the tiger. The cow is red. The cow is round. The rabbit eats the cow. The rabbit needs the cow. The tiger eats the cow. The tiger is kind. The tiger is young. The tiger sees the rabbit. If someone is red and they eat the rabbit then they are kind. If someone needs the rabbit then they are round. If the rabbit needs the cow and the rabbit is cold then the rabbit sees the cow. If someone eats the cat then the cat needs the tiger. If someone needs the cow and they see the cat then the cat is red. If someone needs the cow and the cow eats the rabbit then they see the cat. If someone sees the rabbit then they are red. If someone is young then they see the rabbit.
The cat eats the cow.
("cat" "eats" "cow" "+")
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
The cat eats the tiger.
("cat" "eats" "tiger" "+")
The cat is young.
("cat" "is" "young" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The cow eats the cat.
("cow" "eats" "cat" "+")
The cow eats the tiger.
("cow" "eats" "tiger" "+")
The cow is red.
("cow" "is" "red" "+")
The cow is round.
("cow" "is" "round" "+")
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
The tiger eats the cow.
("tiger" "eats" "cow" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
If someone is red and they eat the rabbit then they are kind.
((("someone" "is" "red" "+") ("someone" "eats" "rabbit" "+")) -> ("someone" "is" "kind" "+"))
If someone needs the rabbit then they are round.
((("someone" "needs" "rabbit" "+")) -> ("someone" "is" "round" "+"))
If the rabbit needs the cow and the rabbit is cold then the rabbit sees the cow.
((("rabbit" "needs" "cow" "+") ("rabbit" "is" "cold" "+")) -> ("rabbit" "sees" "cow" "+"))
If someone eats the cat then the cat needs the tiger.
((("someone" "eats" "cat" "+")) -> ("cat" "needs" "tiger" "+"))
If someone needs the cow and they see the cat then the cat is red.
((("someone" "needs" "cow" "+") ("someone" "sees" "cat" "+")) -> ("cat" "is" "red" "+"))
If someone needs the cow and the cow eats the rabbit then they see the cat.
((("someone" "needs" "cow" "+") ("cow" "eats" "rabbit" "+")) -> ("someone" "sees" "cat" "+"))
If someone sees the rabbit then they are red.
((("someone" "sees" "rabbit" "+")) -> ("someone" "is" "red" "+"))
If someone is young then they see the rabbit.
((("someone" "is" "young" "+")) -> ("someone" "sees" "rabbit" "+"))
The cat is young.
True
1
proof
[(triple4)]
("cat" "is" "young" "+")
triple4
The cat does not eat the cow.
False
1
inv-proof
[(triple1)]
("cat" "eats" "cow" "-")
triple1
The tiger is red.
True
2
proof
[(((triple16) -> rule7) OR ((((triple15) -> rule8)) -> rule7))]
("tiger" "is" "red" "+")
((triple16) -> (rule7 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
((((triple15) -> (rule8 % int2))) -> (rule7 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int2
The cat does not see the rabbit.
False
2
inv-proof
[(((triple4) -> rule8))]
("cat" "sees" "rabbit" "-")
((triple4) -> (rule8 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
The cat is red.
True
3
proof
[(((((triple4) -> rule8)) -> rule7))]
("cat" "is" "red" "+")
((((triple4) -> (rule8 % int2))) -> (rule7 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int2
The cat is not red.
False
3
inv-proof
[(((((triple4) -> rule8)) -> rule7))]
("cat" "is" "red" "-")
((((triple4) -> (rule8 % int2))) -> (rule7 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int2
The cat is kind.
True
5
proof
[(((((((triple4) -> rule8)) -> rule7) triple2) -> rule1))]
("cat" "is" "kind" "+")
((((((triple4) -> (rule8 % int3))) -> (rule7 % int2)) triple2) -> (rule1 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int3
The cat is not kind.
False
5
inv-proof
[(((((((triple4) -> rule8)) -> rule7) triple2) -> rule1))]
("cat" "is" "kind" "-")
((((((triple4) -> (rule8 % int3))) -> (rule7 % int2)) triple2) -> (rule1 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int3
The cow is not kind.
Unknown
inv-rconc
[@1: The cow is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "is" "kind" "-")
The rabbit is red.
Unknown
rconc
[@2: The rabbit is red.[CWA. Example of deepest failure = (rule7 <- rule8 <- FAIL)]]
("rabbit" "is" "red" "+")
The rabbit does not see the cat.
Unknown
inv-rconc
[@1: The rabbit sees the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "sees" "cat" "-")
The tiger sees the cat.
Unknown
rconc
[@1: The tiger sees the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "sees" "cat" "+")
The tiger is not cold.
Unknown
inv-random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
The tiger does not need the cat.
Unknown
inv-random
[@0: The tiger needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "cat" "-")
The cat sees the cow.
Unknown
random
[@0: The cat sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cow" "+")
@0: The cat eats the cow.[(triple1)] The cat eats the rabbit.[(triple2)] The cat eats the tiger.[(triple3)] The cat is young.[(triple4)] The cat needs the cow.[(triple5)] The cat needs the tiger.[(triple6 OR ((triple7) -> rule4))] The cow eats the cat.[(triple7)] The cow eats the tiger.[(triple8)] The cow is red.[(triple9)] The cow is round.[(triple10)] The rabbit eats the cow.[(triple11)] The rabbit needs the cow.[(triple12)] The tiger eats the cow.[(triple13)] The tiger is kind.[(triple14)] The tiger is young.[(triple15)] The tiger sees the rabbit.[(triple16 OR ((triple15) -> rule8))] @1: The cat sees the rabbit.[(((triple4) -> rule8))] The tiger is red.[(((triple16) -> rule7) OR ((((triple15) -> rule8)) -> rule7))] @2: The cat is red.[(((((triple4) -> rule8)) -> rule7))] @3: The cat is kind.[(((((((triple4) -> rule8)) -> rule7) triple2) -> rule1))]
The cat eats the cow.
("cat" "eats" "cow" "+")
triple1
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
triple2
The cat eats the tiger.
("cat" "eats" "tiger" "+")
triple3
The cat is young.
("cat" "is" "young" "+")
triple4
The cat needs the cow.
("cat" "needs" "cow" "+")
triple5
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple6
((triple7) -> (rule4 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
The cow eats the cat.
("cow" "eats" "cat" "+")
triple7
The cow eats the tiger.
("cow" "eats" "tiger" "+")
triple8
The cow is red.
("cow" "is" "red" "+")
triple9
The cow is round.
("cow" "is" "round" "+")
triple10
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
triple11
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple12
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple13
The tiger is kind.
("tiger" "is" "kind" "+")
triple14
The tiger is young.
("tiger" "is" "young" "+")
triple15
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple16
((triple15) -> (rule8 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
((triple4) -> (rule8 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
((triple16) -> (rule7 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
((((triple15) -> (rule8 % int2))) -> (rule7 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int2
The cat is red.
("cat" "is" "red" "+")
((((triple4) -> (rule8 % int2))) -> (rule7 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int2
The cat is kind.
("cat" "is" "kind" "+")
((((((triple4) -> (rule8 % int3))) -> (rule7 % int2)) triple2) -> (rule1 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int3