The cow chases the rabbit. The cow chases the tiger. The cow is big. The cow is red. The cow sees the tiger. The lion chases the tiger. The lion does not see the rabbit. The lion does not see the tiger. The rabbit is not blue. The rabbit is red. The rabbit sees the lion. The tiger chases the cow. If something is big then it is blue. If something is cold then it is blue. If something is blue then it eats the tiger. If something eats the rabbit and the rabbit is big then it is red. If something eats the tiger then the tiger sees the rabbit. If the cow sees the tiger and the tiger sees the rabbit then the tiger is cold. If something is red then it chases the cow. If something is blue and it chases the lion then it chases the rabbit. If something eats the rabbit then it chases the lion.
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
The cow chases the tiger.
("cow" "chases" "tiger" "+")
The cow is big.
("cow" "is" "big" "+")
The cow is red.
("cow" "is" "red" "+")
The cow sees the tiger.
("cow" "sees" "tiger" "+")
The lion chases the tiger.
("lion" "chases" "tiger" "+")
The lion does not see the rabbit.
("lion" "sees" "rabbit" "-")
The lion does not see the tiger.
("lion" "sees" "tiger" "-")
The rabbit is not blue.
("rabbit" "is" "blue" "-")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
The tiger chases the cow.
("tiger" "chases" "cow" "+")
If something is big then it is blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
If something is cold then it is blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
If something is blue then it eats the tiger.
((("something" "is" "blue" "+")) -> ("something" "eats" "tiger" "+"))
If something eats the rabbit and the rabbit is big then it is red.
((("something" "eats" "rabbit" "+") ("rabbit" "is" "big" "+")) -> ("something" "is" "red" "+"))
If something eats the tiger then the tiger sees the rabbit.
((("something" "eats" "tiger" "+")) -> ("tiger" "sees" "rabbit" "+"))
If the cow sees the tiger and the tiger sees the rabbit then the tiger is cold.
((("cow" "sees" "tiger" "+") ("tiger" "sees" "rabbit" "+")) -> ("tiger" "is" "cold" "+"))
If something is red then it chases the cow.
((("something" "is" "red" "+")) -> ("something" "chases" "cow" "+"))
If something is blue and it chases the lion then it chases the rabbit.
((("something" "is" "blue" "+") ("something" "chases" "lion" "+")) -> ("something" "chases" "rabbit" "+"))
If something eats the rabbit then it chases the lion.
((("something" "eats" "rabbit" "+")) -> ("something" "chases" "lion" "+"))
The cow chases the tiger.
True
1
proof
[(triple2)]
("cow" "chases" "tiger" "+")
triple2
The lion sees the rabbit.
False
1
inv-proof
[(triple7)]
("lion" "sees" "rabbit" "+")
triple7
The cow chases the cow.
True
2
proof
[(((triple4) -> rule7))]
("cow" "chases" "cow" "+")
((triple4) -> (rule7 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow does not chase the cow.
False
2
inv-proof
[(((triple4) -> rule7))]
("cow" "chases" "cow" "-")
((triple4) -> (rule7 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow eats the tiger.
True
3
proof
[(((((triple3) -> rule1)) -> rule3))]
("cow" "eats" "tiger" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow does not eat the tiger.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule3))]
("cow" "eats" "tiger" "-")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The tiger sees the rabbit.
True
4
proof
[(((((((triple3) -> rule1)) -> rule3)) -> rule5))]
("tiger" "sees" "rabbit" "+")
((((((triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int2
The cow is blue.
("cow" "is" "blue" "+")
int3
The tiger does not see the rabbit.
False
4
inv-proof
[(((((((triple3) -> rule1)) -> rule3)) -> rule5))]
("tiger" "sees" "rabbit" "-")
((((((triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int2
The cow is blue.
("cow" "is" "blue" "+")
int3
The tiger is cold.
True
6
proof
[(((triple5 ((((((triple3) -> rule1)) -> rule3)) -> rule5)) -> rule6))]
("tiger" "is" "cold" "+")
((triple5 ((((((triple3) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int2
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int3
The cow is blue.
("cow" "is" "blue" "+")
int4
The tiger is not cold.
False
6
inv-proof
[(((triple5 ((((((triple3) -> rule1)) -> rule3)) -> rule5)) -> rule6))]
("tiger" "is" "cold" "-")
((triple5 ((((((triple3) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int2
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int3
The cow is blue.
("cow" "is" "blue" "+")
int4
The tiger is blue.
True
7
proof
[(((((triple5 ((((((triple3) -> rule1)) -> rule3)) -> rule5)) -> rule6)) -> rule2))]
("tiger" "is" "blue" "+")
((((triple5 ((((((triple3) -> (rule1 % int5))) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int3
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int4
The cow is blue.
("cow" "is" "blue" "+")
int5
The tiger is not blue.
False
7
inv-proof
[(((((triple5 ((((((triple3) -> rule1)) -> rule3)) -> rule5)) -> rule6)) -> rule2))]
("tiger" "is" "blue" "-")
((((triple5 ((((((triple3) -> (rule1 % int5))) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int3
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int4
The cow is blue.
("cow" "is" "blue" "+")
int5
The lion does not chase the cow.
Unknown
inv-rconc
[@2: The lion chases the cow.[CWA. Example of deepest failure = (rule7 <- rule4 <- FAIL)]]
("lion" "chases" "cow" "-")
The rabbit chases the rabbit.
Unknown
rconc
[@1: The rabbit chases the rabbit.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "chases" "rabbit" "+")
The lion does not eat the tiger.
Unknown
inv-rconc
[@2: The lion eats the tiger.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("lion" "eats" "tiger" "-")
The lion chases the rabbit.
Unknown
rconc
[@2: The lion chases the rabbit.[CWA. Example of deepest failure = (rule8 <- rule1 <- FAIL)]]
("lion" "chases" "rabbit" "+")
The tiger does not chase the lion.
Unknown
inv-rconc
[@1: The tiger chases the lion.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("tiger" "chases" "lion" "-")
The lion chases the lion.
Unknown
rconc
[@1: The lion chases the lion.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("lion" "chases" "lion" "+")
The tiger does not see the lion.
Unknown
inv-random
[@0: The tiger sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "lion" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
The lion is not cold.
Unknown
inv-random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "-")
The rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
The lion is not big.
Unknown
inv-random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "-")
The rabbit eats the cow.
Unknown
random
[@0: The rabbit eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "cow" "+")
@0: The cow chases the rabbit.[(triple1)] The cow chases the tiger.[(triple2)] The cow is big.[(triple3)] The cow is red.[(triple4)] The cow sees the tiger.[(triple5)] The lion chases the tiger.[(triple6)] The lion does not see the rabbit.[(triple7)] The lion does not see the tiger.[(triple8)] The rabbit is not blue.[(triple9)] The rabbit is red.[(triple10)] The rabbit sees the lion.[(triple11)] The tiger chases the cow.[(triple12)] @1: The cow chases the cow.[(((triple4) -> rule7))] The cow is blue.[(((triple3) -> rule1))] The rabbit chases the cow.[(((triple10) -> rule7))] @2: The cow eats the tiger.[(((((triple3) -> rule1)) -> rule3))] @3: The tiger sees the rabbit.[(((((((triple3) -> rule1)) -> rule3)) -> rule5))] @4: The tiger is cold.[(((triple5 ((((((triple3) -> rule1)) -> rule3)) -> rule5)) -> rule6))] @5: The tiger is blue.[(((((triple5 ((((((triple3) -> rule1)) -> rule3)) -> rule5)) -> rule6)) -> rule2))] @6: The tiger eats the tiger.[(((((((triple5 ((((((triple3) -> rule1)) -> rule3)) -> rule5)) -> rule6)) -> rule2)) -> rule3))]
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
triple1
The cow chases the tiger.
("cow" "chases" "tiger" "+")
triple2
The cow is big.
("cow" "is" "big" "+")
triple3
The cow is red.
("cow" "is" "red" "+")
triple4
The cow sees the tiger.
("cow" "sees" "tiger" "+")
triple5
The lion chases the tiger.
("lion" "chases" "tiger" "+")
triple6
The lion does not see the rabbit.
("lion" "sees" "rabbit" "-")
triple7
The lion does not see the tiger.
("lion" "sees" "tiger" "-")
triple8
The rabbit is not blue.
("rabbit" "is" "blue" "-")
triple9
The rabbit is red.
("rabbit" "is" "red" "+")
triple10
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple11
The tiger chases the cow.
("tiger" "chases" "cow" "+")
triple12
The cow chases the cow.
("cow" "chases" "cow" "+")
((triple4) -> (rule7 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
((triple3) -> (rule1 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
((triple10) -> (rule7 % int1))
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int1
The cow eats the tiger.
("cow" "eats" "tiger" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
((((((triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int2
The cow is blue.
("cow" "is" "blue" "+")
int3
The tiger is cold.
("tiger" "is" "cold" "+")
((triple5 ((((((triple3) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int2
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int3
The cow is blue.
("cow" "is" "blue" "+")
int4
The tiger is blue.
("tiger" "is" "blue" "+")
((((triple5 ((((((triple3) -> (rule1 % int5))) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int3
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int4
The cow is blue.
("cow" "is" "blue" "+")
int5
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((((((triple5 ((((((triple3) -> (rule1 % int6))) -> (rule3 % int5))) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
int3
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int4
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int5
The cow is blue.
("cow" "is" "blue" "+")
int6