The cow is big. The cow visits the mouse. The lion needs the mouse. The lion visits the mouse. The mouse is not red. The mouse is young. The tiger does not visit the lion. If the tiger does not need the cow and the cow is not rough then the cow visits the tiger. If someone visits the cow then they are blue. If someone eats the lion then they are blue. If the cow visits the mouse then the cow is red. If someone is red then they need the lion. If someone is red and they visit the lion then they eat the lion. If someone needs the lion then the lion visits the cow. If someone is blue then they are red. If someone visits the lion then the lion needs the tiger.
The cow is big.
("cow" "is" "big" "+")
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The mouse is not red.
("mouse" "is" "red" "-")
The mouse is young.
("mouse" "is" "young" "+")
The tiger does not visit the lion.
("tiger" "visits" "lion" "-")
If the tiger does not need the cow and the cow is not rough then the cow visits the tiger.
((("tiger" "needs" "cow" "~") ("cow" "is" "rough" "~")) -> ("cow" "visits" "tiger" "+"))
If someone visits the cow then they are blue.
((("someone" "visits" "cow" "+")) -> ("someone" "is" "blue" "+"))
If someone eats the lion then they are blue.
((("someone" "eats" "lion" "+")) -> ("someone" "is" "blue" "+"))
If the cow visits the mouse then the cow is red.
((("cow" "visits" "mouse" "+")) -> ("cow" "is" "red" "+"))
If someone is red then they need the lion.
((("someone" "is" "red" "+")) -> ("someone" "needs" "lion" "+"))
If someone is red and they visit the lion then they eat the lion.
((("someone" "is" "red" "+") ("someone" "visits" "lion" "+")) -> ("someone" "eats" "lion" "+"))
If someone needs the lion then the lion visits the cow.
((("someone" "needs" "lion" "+")) -> ("lion" "visits" "cow" "+"))
If someone is blue then they are red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
If someone visits the lion then the lion needs the tiger.
((("someone" "visits" "lion" "+")) -> ("lion" "needs" "tiger" "+"))
The lion needs the mouse.
True
1
proof
[(triple3)]
("lion" "needs" "mouse" "+")
triple3
The tiger visits the lion.
False
1
inv-proof
[(triple7)]
("tiger" "visits" "lion" "+")
triple7
The cow is red.
True
2
proof
[(((triple2) -> rule4))]
("cow" "is" "red" "+")
((triple2) -> (rule4 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is not red.
False
2
inv-proof
[(((triple2) -> rule4))]
("cow" "is" "red" "-")
((triple2) -> (rule4 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow needs the lion.
True
3
proof
[(((((triple2) -> rule4)) -> rule5))]
("cow" "needs" "lion" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The cow needs the lion.
("cow" "needs" "lion" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow does not need the lion.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule5))]
("cow" "needs" "lion" "-")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The cow needs the lion.
("cow" "needs" "lion" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The lion visits the cow.
True
4
proof
[(((((((triple2) -> rule4)) -> rule5)) -> rule7))]
("lion" "visits" "cow" "+")
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The lion visits the cow.
("lion" "visits" "cow" "+")
int1
The cow needs the lion.
("cow" "needs" "lion" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The lion does not visit the cow.
False
4
inv-proof
[(((((((triple2) -> rule4)) -> rule5)) -> rule7))]
("lion" "visits" "cow" "-")
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The lion visits the cow.
("lion" "visits" "cow" "+")
int1
The cow needs the lion.
("cow" "needs" "lion" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The lion is blue.
True
5
proof
[(((((((((triple2) -> rule4)) -> rule5)) -> rule7)) -> rule2))]
("lion" "is" "blue" "+")
((((((((triple2) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion visits the cow.
("lion" "visits" "cow" "+")
int2
The cow needs the lion.
("cow" "needs" "lion" "+")
int3
The cow is red.
("cow" "is" "red" "+")
int4
The lion is not blue.
False
5
inv-proof
[(((((((((triple2) -> rule4)) -> rule5)) -> rule7)) -> rule2))]
("lion" "is" "blue" "-")
((((((((triple2) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion visits the cow.
("lion" "visits" "cow" "+")
int2
The cow needs the lion.
("cow" "needs" "lion" "+")
int3
The cow is red.
("cow" "is" "red" "+")
int4
The lion is red.
True
6
proof
[(((((((((((triple2) -> rule4)) -> rule5)) -> rule7)) -> rule2)) -> rule8))]
("lion" "is" "red" "+")
((((((((((triple2) -> (rule4 % int5))) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion visits the cow.
("lion" "visits" "cow" "+")
int3
The cow needs the lion.
("cow" "needs" "lion" "+")
int4
The cow is red.
("cow" "is" "red" "+")
int5
The lion is not red.
False
6
inv-proof
[(((((((((((triple2) -> rule4)) -> rule5)) -> rule7)) -> rule2)) -> rule8))]
("lion" "is" "red" "-")
((((((((((triple2) -> (rule4 % int5))) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion visits the cow.
("lion" "visits" "cow" "+")
int3
The cow needs the lion.
("cow" "needs" "lion" "+")
int4
The cow is red.
("cow" "is" "red" "+")
int5
The lion does not need the tiger.
Unknown
inv-rconc
[@1: The lion needs the tiger.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("lion" "needs" "tiger" "-")
The cow visits the tiger.
Unknown
rconc
[@1: The cow visits the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "visits" "tiger" "+")
The cow is not blue.
Unknown
inv-rconc
[@2: The cow is blue.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("cow" "is" "blue" "-")
The mouse needs the lion.
Unknown
rconc
[@1: The mouse needs the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "needs" "lion" "+")
The tiger is not blue.
Unknown
inv-rconc
[@2: The tiger is blue.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("tiger" "is" "blue" "-")
The mouse is blue.
Unknown
rconc
[@2: The mouse is blue.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("mouse" "is" "blue" "+")
The lion is not big.
Unknown
inv-random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "-")
The tiger is rough.
Unknown
random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "+")
The lion is not young.
Unknown
inv-random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
The cow does not visit the lion.
Unknown
inv-random
[@0: The cow visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "lion" "-")
The lion eats the cow.
Unknown
random
[@0: The lion eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "cow" "+")
@0: The cow is big.[(triple1)] The cow visits the mouse.[(triple2)] The lion needs the mouse.[(triple3)] The lion visits the mouse.[(triple4)] The mouse is not red.[(triple5)] The mouse is young.[(triple6)] The tiger does not visit the lion.[(triple7)] @1: The cow is red.[(((triple2) -> rule4))] @2: The cow needs the lion.[(((((triple2) -> rule4)) -> rule5))] @3: The lion visits the cow.[(((((((triple2) -> rule4)) -> rule5)) -> rule7))] @4: The lion is blue.[(((((((((triple2) -> rule4)) -> rule5)) -> rule7)) -> rule2))] @5: The lion is red.[(((((((((((triple2) -> rule4)) -> rule5)) -> rule7)) -> rule2)) -> rule8))] @6: The lion needs the lion.[(((((((((((((triple2) -> rule4)) -> rule5)) -> rule7)) -> rule2)) -> rule8)) -> rule5))]
The cow is big.
("cow" "is" "big" "+")
triple1
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple2
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple3
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple4
The mouse is not red.
("mouse" "is" "red" "-")
triple5
The mouse is young.
("mouse" "is" "young" "+")
triple6
The tiger does not visit the lion.
("tiger" "visits" "lion" "-")
triple7
The cow is red.
("cow" "is" "red" "+")
((triple2) -> (rule4 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow needs the lion.
("cow" "needs" "lion" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The cow needs the lion.
("cow" "needs" "lion" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The lion visits the cow.
("lion" "visits" "cow" "+")
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The lion visits the cow.
("lion" "visits" "cow" "+")
int1
The cow needs the lion.
("cow" "needs" "lion" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The lion is blue.
("lion" "is" "blue" "+")
((((((((triple2) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion visits the cow.
("lion" "visits" "cow" "+")
int2
The cow needs the lion.
("cow" "needs" "lion" "+")
int3
The cow is red.
("cow" "is" "red" "+")
int4
The lion is red.
("lion" "is" "red" "+")
((((((((((triple2) -> (rule4 % int5))) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion visits the cow.
("lion" "visits" "cow" "+")
int3
The cow needs the lion.
("cow" "needs" "lion" "+")
int4
The cow is red.
("cow" "is" "red" "+")
int5
The lion needs the lion.
("lion" "needs" "lion" "+")
((((((((((((triple2) -> (rule4 % int6))) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
int3
The lion visits the cow.
("lion" "visits" "cow" "+")
int4
The cow needs the lion.
("cow" "needs" "lion" "+")
int5
The cow is red.
("cow" "is" "red" "+")
int6