The bear eats the rabbit. The bear is cold. The lion is cold. The mouse chases the bear. The mouse does not like the rabbit. The rabbit chases the mouse. The rabbit is red. If someone eats the rabbit then the rabbit does not chase the bear. If someone chases the mouse then the mouse does not like the bear. If someone is young then they chase the mouse. If someone is big then they like the rabbit. If someone chases the mouse then they are big. If the lion is cold then the lion is young. If someone is big and young then they chase the bear. If someone chases the bear then they chase the lion. If the mouse is not red and the mouse does not chase the lion then the lion is not red.
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
The bear is cold.
("bear" "is" "cold" "+")
The lion is cold.
("lion" "is" "cold" "+")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
The mouse does not like the rabbit.
("mouse" "likes" "rabbit" "-")
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
If someone eats the rabbit then the rabbit does not chase the bear.
((("someone" "eats" "rabbit" "+")) -> ("rabbit" "chases" "bear" "-"))
If someone chases the mouse then the mouse does not like the bear.
((("someone" "chases" "mouse" "+")) -> ("mouse" "likes" "bear" "-"))
If someone is young then they chase the mouse.
((("someone" "is" "young" "+")) -> ("someone" "chases" "mouse" "+"))
If someone is big then they like the rabbit.
((("someone" "is" "big" "+")) -> ("someone" "likes" "rabbit" "+"))
If someone chases the mouse then they are big.
((("someone" "chases" "mouse" "+")) -> ("someone" "is" "big" "+"))
If the lion is cold then the lion is young.
((("lion" "is" "cold" "+")) -> ("lion" "is" "young" "+"))
If someone is big and young then they chase the bear.
((("someone" "is" "big" "+") ("someone" "is" "young" "+")) -> ("someone" "chases" "bear" "+"))
If someone chases the bear then they chase the lion.
((("someone" "chases" "bear" "+")) -> ("someone" "chases" "lion" "+"))
If the mouse is not red and the mouse does not chase the lion then the lion is not red.
((("mouse" "is" "red" "~") ("mouse" "chases" "lion" "~")) -> ("lion" "is" "red" "-"))
The rabbit chases the mouse.
True
1
proof
[(triple6)]
("rabbit" "chases" "mouse" "+")
triple6
The rabbit does not chase the mouse.
False
1
inv-proof
[(triple6)]
("rabbit" "chases" "mouse" "-")
triple6
The mouse chases the lion.
True
2
proof
[(((triple4) -> rule8))]
("mouse" "chases" "lion" "+")
((triple4) -> (rule8 % int1))
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int1
The rabbit is not big.
False
2
inv-proof
[(((triple6) -> rule5))]
("rabbit" "is" "big" "-")
((triple6) -> (rule5 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The lion chases the mouse.
True
3
proof
[(((((triple3) -> rule6)) -> rule3))]
("lion" "chases" "mouse" "+")
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The rabbit does not like the rabbit.
False
3
inv-proof
[(((((triple6) -> rule5)) -> rule4))]
("rabbit" "likes" "rabbit" "-")
((((triple6) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The lion is big.
True
4
proof
[(((((((triple3) -> rule6)) -> rule3)) -> rule5))]
("lion" "is" "big" "+")
((((((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The lion is not big.
False
4
inv-proof
[(((((((triple3) -> rule6)) -> rule3)) -> rule5))]
("lion" "is" "big" "-")
((((((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The lion chases the bear.
True
7
proof
[(((((((((triple3) -> rule6)) -> rule3)) -> rule5) ((triple3) -> rule6)) -> rule7))]
("lion" "chases" "bear" "+")
((((((((triple3) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) ((triple3) -> (rule6 % int4))) -> (rule7 % int1))
The lion chases the bear.
("lion" "chases" "bear" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int3
The lion is young.
("lion" "is" "young" "+")
int4
The lion does not chase the bear.
False
7
inv-proof
[(((((((((triple3) -> rule6)) -> rule3)) -> rule5) ((triple3) -> rule6)) -> rule7))]
("lion" "chases" "bear" "-")
((((((((triple3) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) ((triple3) -> (rule6 % int4))) -> (rule7 % int1))
The lion chases the bear.
("lion" "chases" "bear" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int3
The lion is young.
("lion" "is" "young" "+")
int4
The lion chases the lion.
True
8
proof
[(((((((((((triple3) -> rule6)) -> rule3)) -> rule5) ((triple3) -> rule6)) -> rule7)) -> rule8))]
("lion" "chases" "lion" "+")
((((((((((triple3) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule5 % int3)) ((triple3) -> (rule6 % int5))) -> (rule7 % int2))) -> (rule8 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion chases the bear.
("lion" "chases" "bear" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int4
The lion is young.
("lion" "is" "young" "+")
int5
The lion does not chase the lion.
False
8
inv-proof
[(((((((((((triple3) -> rule6)) -> rule3)) -> rule5) ((triple3) -> rule6)) -> rule7)) -> rule8))]
("lion" "chases" "lion" "-")
((((((((((triple3) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule5 % int3)) ((triple3) -> (rule6 % int5))) -> (rule7 % int2))) -> (rule8 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion chases the bear.
("lion" "chases" "bear" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int4
The lion is young.
("lion" "is" "young" "+")
int5
The mouse is not big.
Unknown
inv-rconc
[@2: The mouse is big.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("mouse" "is" "big" "-")
The mouse chases the mouse.
Unknown
rconc
[@1: The mouse chases the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "chases" "mouse" "+")
The bear does not chase the mouse.
Unknown
inv-rconc
[@1: The bear chases the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "chases" "mouse" "-")
The bear chases the lion.
Unknown
rconc
[@2: The bear chases the lion.[CWA. Example of deepest failure = (rule8 <- rule7 <- FAIL)]]
("bear" "chases" "lion" "+")
The bear does not like the rabbit.
Unknown
inv-rconc
[@3: The bear likes the rabbit.[CWA. Example of deepest failure = (rule4 <- rule5 <- rule3 <- FAIL)]]
("bear" "likes" "rabbit" "-")
The bear is big.
Unknown
rconc
[@2: The bear is big.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("bear" "is" "big" "+")
The mouse is not red.
Unknown
inv-random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "-")
The mouse likes the lion.
Unknown
random
[@0: The mouse likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "lion" "+")
The rabbit does not chase the rabbit.
Unknown
inv-random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "-")
The lion likes the mouse.
Unknown
random
[@0: The lion likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "mouse" "+")
The bear is not young.
Unknown
inv-random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "young" "-")
The mouse is cold.
Unknown
random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "+")
@0: The bear eats the rabbit.[(triple1)] The bear is cold.[(triple2)] The lion is cold.[(triple3)] The mouse chases the bear.[(triple4)] The mouse does not like the rabbit.[(triple5)] The rabbit chases the mouse.[(triple6)] The rabbit is red.[(triple7)] @1: The lion is young.[(((triple3) -> rule6))] The mouse chases the lion.[(((triple4) -> rule8))] The mouse does not like the bear.[(((triple6) -> rule2) OR ((((((triple3) -> rule6)) -> rule3)) -> rule2))] The rabbit does not chase the bear.[(((triple1) -> rule1))] The rabbit is big.[(((triple6) -> rule5))] @2: The lion chases the mouse.[(((((triple3) -> rule6)) -> rule3))] The rabbit likes the rabbit.[(((((triple6) -> rule5)) -> rule4))] @3: The lion is big.[(((((((triple3) -> rule6)) -> rule3)) -> rule5))] @4: The lion chases the bear.[(((((((((triple3) -> rule6)) -> rule3)) -> rule5) ((triple3) -> rule6)) -> rule7))] The lion likes the rabbit.[(((((((((triple3) -> rule6)) -> rule3)) -> rule5)) -> rule4))] @5: The lion chases the lion.[(((((((((((triple3) -> rule6)) -> rule3)) -> rule5) ((triple3) -> rule6)) -> rule7)) -> rule8))]
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
triple1
The bear is cold.
("bear" "is" "cold" "+")
triple2
The lion is cold.
("lion" "is" "cold" "+")
triple3
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple4
The mouse does not like the rabbit.
("mouse" "likes" "rabbit" "-")
triple5
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
triple6
The rabbit is red.
("rabbit" "is" "red" "+")
triple7
The lion is young.
("lion" "is" "young" "+")
((triple3) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The mouse chases the lion.
("mouse" "chases" "lion" "+")
((triple4) -> (rule8 % int1))
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int1
The mouse does not like the bear.
("mouse" "likes" "bear" "-")
((triple6) -> (rule2 % int1))
The mouse does not like the bear.
("mouse" "likes" "bear" "-")
int1
((((((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The mouse does not like the bear.
("mouse" "likes" "bear" "-")
int1
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The rabbit does not chase the bear.
("rabbit" "chases" "bear" "-")
((triple1) -> (rule1 % int1))
The rabbit does not chase the bear.
("rabbit" "chases" "bear" "-")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
((triple6) -> (rule5 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The lion chases the mouse.
("lion" "chases" "mouse" "+")
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
((((triple6) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The lion is big.
("lion" "is" "big" "+")
((((((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The lion chases the bear.
("lion" "chases" "bear" "+")
((((((((triple3) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) ((triple3) -> (rule6 % int4))) -> (rule7 % int1))
The lion chases the bear.
("lion" "chases" "bear" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int3
The lion is young.
("lion" "is" "young" "+")
int4
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
((((((((triple3) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int3
The lion is young.
("lion" "is" "young" "+")
int4
The lion chases the lion.
("lion" "chases" "lion" "+")
((((((((((triple3) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule5 % int3)) ((triple3) -> (rule6 % int5))) -> (rule7 % int2))) -> (rule8 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion chases the bear.
("lion" "chases" "bear" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int4
The lion is young.
("lion" "is" "young" "+")
int5