The bear chases the mouse. The bear eats the mouse. The bear is rough. The bear needs the mouse. The mouse chases the bear. The mouse eats the bear. The mouse eats the tiger. The mouse is red. The mouse needs the tiger. The tiger chases the bear. The tiger chases the mouse. The tiger eats the bear. The tiger eats the mouse. The tiger is not red. The tiger needs the bear. The tiger does not need the mouse. If something chases the mouse then it is cold. If the bear needs the tiger then the tiger is rough. If something is cold then it chases the tiger.
The bear chases the mouse.
("bear" "chases" "mouse" "+")
The bear eats the mouse.
("bear" "eats" "mouse" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
The mouse eats the bear.
("mouse" "eats" "bear" "+")
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The tiger chases the bear.
("tiger" "chases" "bear" "+")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
The tiger eats the bear.
("tiger" "eats" "bear" "+")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
The tiger is not red.
("tiger" "is" "red" "-")
The tiger needs the bear.
("tiger" "needs" "bear" "+")
The tiger does not need the mouse.
("tiger" "needs" "mouse" "-")
If something chases the mouse then it is cold.
((("something" "chases" "mouse" "+")) -> ("something" "is" "cold" "+"))
If the bear needs the tiger then the tiger is rough.
((("bear" "needs" "tiger" "+")) -> ("tiger" "is" "rough" "+"))
If something is cold then it chases the tiger.
((("something" "is" "cold" "+")) -> ("something" "chases" "tiger" "+"))
The tiger eats the bear.
True
1
proof
[(triple12)]
("tiger" "eats" "bear" "+")
triple12
The mouse does not eat the bear.
False
1
inv-proof
[(triple6)]
("mouse" "eats" "bear" "-")
triple6
The tiger is cold.
True
2
proof
[(((triple11) -> rule1))]
("tiger" "is" "cold" "+")
((triple11) -> (rule1 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is not cold.
False
2
inv-proof
[(((triple11) -> rule1))]
("tiger" "is" "cold" "-")
((triple11) -> (rule1 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger chases the tiger.
True
3
proof
[(((((triple11) -> rule1)) -> rule3))]
("tiger" "chases" "tiger" "+")
((((triple11) -> (rule1 % int2))) -> (rule3 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The bear does not chase the tiger.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("bear" "chases" "tiger" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The mouse is not cold.
Unknown
inv-rconc
[@1: The mouse is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "cold" "-")
The mouse chases the tiger.
Unknown
rconc
[@2: The mouse chases the tiger.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("mouse" "chases" "tiger" "+")
The tiger is not rough.
Unknown
inv-rconc
[@1: The tiger is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "rough" "-")
The bear needs the bear.
Unknown
random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "+")
The mouse does not chase the mouse.
Unknown
inv-random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "-")
The bear eats the bear.
Unknown
random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "+")
@0: The bear chases the mouse.[(triple1)] The bear eats the mouse.[(triple2)] The bear is rough.[(triple3)] The bear needs the mouse.[(triple4)] The mouse chases the bear.[(triple5)] The mouse eats the bear.[(triple6)] The mouse eats the tiger.[(triple7)] The mouse is red.[(triple8)] The mouse needs the tiger.[(triple9)] The tiger chases the bear.[(triple10)] The tiger chases the mouse.[(triple11)] The tiger does not need the mouse.[(triple16)] The tiger eats the bear.[(triple12)] The tiger eats the mouse.[(triple13)] The tiger is not red.[(triple14)] The tiger needs the bear.[(triple15)] @1: The bear is cold.[(((triple1) -> rule1))] The tiger is cold.[(((triple11) -> rule1))] @2: The bear chases the tiger.[(((((triple1) -> rule1)) -> rule3))] The tiger chases the tiger.[(((((triple11) -> rule1)) -> rule3))]
The bear chases the mouse.
("bear" "chases" "mouse" "+")
triple1
The bear eats the mouse.
("bear" "eats" "mouse" "+")
triple2
The bear is rough.
("bear" "is" "rough" "+")
triple3
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple4
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple5
The mouse eats the bear.
("mouse" "eats" "bear" "+")
triple6
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple7
The mouse is red.
("mouse" "is" "red" "+")
triple8
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple9
The tiger chases the bear.
("tiger" "chases" "bear" "+")
triple10
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple11
The tiger does not need the mouse.
("tiger" "needs" "mouse" "-")
triple16
The tiger eats the bear.
("tiger" "eats" "bear" "+")
triple12
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple13
The tiger is not red.
("tiger" "is" "red" "-")
triple14
The tiger needs the bear.
("tiger" "needs" "bear" "+")
triple15
The bear is cold.
("bear" "is" "cold" "+")
((triple1) -> (rule1 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
((triple11) -> (rule1 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
((((triple11) -> (rule1 % int2))) -> (rule3 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2