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