The bear does not chase the rabbit. The bear does not eat the tiger. The bear is green. The bear is rough. The bear likes the mouse. The mouse does not chase the rabbit. The mouse chases the tiger. The mouse eats the rabbit. The mouse eats the tiger. The mouse is not blue. The mouse is red. The mouse likes the bear. The mouse likes the rabbit. The rabbit eats the mouse. The rabbit likes the tiger. The tiger likes the mouse. Rough things are red. If something is rough and it eats the tiger then the tiger is rough. If something likes the tiger then it is rough. If something eats the bear and the bear eats the tiger then the bear chases the mouse. If something is cold and red then it eats the rabbit. If something eats the bear then it is blue. If something is red then it chases the mouse. If something chases the mouse and the mouse likes the rabbit then it likes the tiger.
The bear does not chase the rabbit.
("bear" "chases" "rabbit" "-")
The bear does not eat the tiger.
("bear" "eats" "tiger" "-")
The bear is green.
("bear" "is" "green" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear likes the mouse.
("bear" "likes" "mouse" "+")
The mouse does not chase the rabbit.
("mouse" "chases" "rabbit" "-")
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse is not blue.
("mouse" "is" "blue" "-")
The mouse is red.
("mouse" "is" "red" "+")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
Rough things are red.
((("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
If something is rough and it eats the tiger then the tiger is rough.
((("something" "is" "rough" "+") ("something" "eats" "tiger" "+")) -> ("tiger" "is" "rough" "+"))
If something likes the tiger then it is rough.
((("something" "likes" "tiger" "+")) -> ("something" "is" "rough" "+"))
If something eats the bear and the bear eats the tiger then the bear chases the mouse.
((("something" "eats" "bear" "+") ("bear" "eats" "tiger" "+")) -> ("bear" "chases" "mouse" "+"))
If something is cold and red then it eats the rabbit.
((("something" "is" "cold" "+") ("something" "is" "red" "+")) -> ("something" "eats" "rabbit" "+"))
If something eats the bear then it is blue.
((("something" "eats" "bear" "+")) -> ("something" "is" "blue" "+"))
If something is red then it chases the mouse.
((("something" "is" "red" "+")) -> ("something" "chases" "mouse" "+"))
If something chases the mouse and the mouse likes the rabbit then it likes the tiger.
((("something" "chases" "mouse" "+") ("mouse" "likes" "rabbit" "+")) -> ("something" "likes" "tiger" "+"))
The bear is rough.
True
1
proof
[(triple4)]
("bear" "is" "rough" "+")
triple4
The rabbit does not like the tiger.
False
1
inv-proof
[(triple15)]
("rabbit" "likes" "tiger" "-")
triple15
The mouse chases the mouse.
True
2
proof
[(((triple11) -> rule7))]
("mouse" "chases" "mouse" "+")
((triple11) -> (rule7 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The rabbit is not rough.
False
2
inv-proof
[(((triple15) -> rule3))]
("rabbit" "is" "rough" "-")
((triple15) -> (rule3 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The bear chases the mouse.
True
3
proof
[(((((triple4) -> rule1)) -> rule7))]
("bear" "chases" "mouse" "+")
((((triple4) -> (rule1 % int2))) -> (rule7 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The rabbit is not red.
False
3
inv-proof
[(((((triple15) -> rule3)) -> rule1))]
("rabbit" "is" "red" "-")
((((triple15) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The rabbit chases the mouse.
True
4
proof
[(((((((triple15) -> rule3)) -> rule1)) -> rule7))]
("rabbit" "chases" "mouse" "+")
((((((triple15) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit is rough.
("rabbit" "is" "rough" "+")
int3
The mouse is not rough.
False
5
inv-proof
[(((((((triple11) -> rule7) triple13) -> rule8)) -> rule3))]
("mouse" "is" "rough" "-")
((((((triple11) -> (rule7 % int3)) triple13) -> (rule8 % int2))) -> (rule3 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int3
The tiger is rough.
True
7
proof
[(((((((((triple11) -> rule7) triple13) -> rule8)) -> rule3) triple9) -> rule2))]
("tiger" "is" "rough" "+")
((((((((triple11) -> (rule7 % int4)) triple13) -> (rule8 % int3))) -> (rule3 % int2)) triple9) -> (rule2 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int3
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int4
The tiger is not rough.
False
7
inv-proof
[(((((((((triple11) -> rule7) triple13) -> rule8)) -> rule3) triple9) -> rule2))]
("tiger" "is" "rough" "-")
((((((((triple11) -> (rule7 % int4)) triple13) -> (rule8 % int3))) -> (rule3 % int2)) triple9) -> (rule2 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int3
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int4
The tiger is red.
True
8
proof
[(((((((((((triple11) -> rule7) triple13) -> rule8)) -> rule3) triple9) -> rule2)) -> rule1))]
("tiger" "is" "red" "+")
((((((((((triple11) -> (rule7 % int5)) triple13) -> (rule8 % int4))) -> (rule3 % int3)) triple9) -> (rule2 % int2))) -> (rule1 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int4
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int5
The tiger is not red.
False
8
inv-proof
[(((((((((((triple11) -> rule7) triple13) -> rule8)) -> rule3) triple9) -> rule2)) -> rule1))]
("tiger" "is" "red" "-")
((((((((((triple11) -> (rule7 % int5)) triple13) -> (rule8 % int4))) -> (rule3 % int3)) triple9) -> (rule2 % int2))) -> (rule1 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int4
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int5
The rabbit is not blue.
Unknown
inv-rconc
[@1: The rabbit is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "is" "blue" "-")
The bear is blue.
Unknown
rconc
[@1: The bear is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "is" "blue" "+")
The tiger does not eat the rabbit.
Unknown
inv-rconc
[@1: The tiger eats the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "eats" "rabbit" "-")
The tiger is blue.
Unknown
rconc
[@1: The tiger is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "is" "blue" "+")
The bear does not eat the rabbit.
Unknown
inv-rconc
[@1: The bear eats the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "eats" "rabbit" "-")
The rabbit eats the rabbit.
Unknown
rconc
[@1: The rabbit eats the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "eats" "rabbit" "+")
The tiger does not eat the mouse.
Unknown
inv-random
[@0: The tiger eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "mouse" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
The rabbit does not like the bear.
Unknown
inv-random
[@0: The rabbit likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "bear" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
The mouse does not chase the bear.
Unknown
inv-random
[@0: The mouse chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "bear" "-")
The rabbit is green.
Unknown
random
[@0: The rabbit is green.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "green" "+")
@0: The bear does not chase the rabbit.[(triple1)] The bear does not eat the tiger.[(triple2)] The bear is green.[(triple3)] The bear is rough.[(triple4)] The bear likes the mouse.[(triple5)] The mouse chases the tiger.[(triple7)] The mouse does not chase the rabbit.[(triple6)] The mouse eats the rabbit.[(triple8)] The mouse eats the tiger.[(triple9)] The mouse is not blue.[(triple10)] The mouse is red.[(triple11)] The mouse likes the bear.[(triple12)] The mouse likes the rabbit.[(triple13)] The rabbit eats the mouse.[(triple14)] The rabbit likes the tiger.[(triple15)] The tiger likes the mouse.[(triple16)] @1: The bear is red.[(((triple4) -> rule1))] The mouse chases the mouse.[(((triple11) -> rule7))] The rabbit is rough.[(((triple15) -> rule3))] @2: The bear chases the mouse.[(((((triple4) -> rule1)) -> rule7))] The mouse likes the tiger.[(((((triple11) -> rule7) triple13) -> rule8))] The rabbit is red.[(((((triple15) -> rule3)) -> rule1))] @3: The bear likes the tiger.[(((((((triple4) -> rule1)) -> rule7) triple13) -> rule8))] The mouse is rough.[(((((((triple11) -> rule7) triple13) -> rule8)) -> rule3))] The rabbit chases the mouse.[(((((((triple15) -> rule3)) -> rule1)) -> rule7))] @4: The tiger is rough.[(((((((((triple11) -> rule7) triple13) -> rule8)) -> rule3) triple9) -> rule2))] @5: The tiger is red.[(((((((((((triple11) -> rule7) triple13) -> rule8)) -> rule3) triple9) -> rule2)) -> rule1))] @6: The tiger chases the mouse.[(((((((((((((triple11) -> rule7) triple13) -> rule8)) -> rule3) triple9) -> rule2)) -> rule1)) -> rule7))] @7: The tiger likes the tiger.[(((((((((((((((triple11) -> rule7) triple13) -> rule8)) -> rule3) triple9) -> rule2)) -> rule1)) -> rule7) triple13) -> rule8))]
The bear does not chase the rabbit.
("bear" "chases" "rabbit" "-")
triple1
The bear does not eat the tiger.
("bear" "eats" "tiger" "-")
triple2
The bear is green.
("bear" "is" "green" "+")
triple3
The bear is rough.
("bear" "is" "rough" "+")
triple4
The bear likes the mouse.
("bear" "likes" "mouse" "+")
triple5
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple7
The mouse does not chase the rabbit.
("mouse" "chases" "rabbit" "-")
triple6
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
triple8
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple9
The mouse is not blue.
("mouse" "is" "blue" "-")
triple10
The mouse is red.
("mouse" "is" "red" "+")
triple11
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple12
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
triple13
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
triple14
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple15
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple16
The bear is red.
("bear" "is" "red" "+")
((triple4) -> (rule1 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((triple11) -> (rule7 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
((triple15) -> (rule3 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
((((triple4) -> (rule1 % int2))) -> (rule7 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
((((triple11) -> (rule7 % int2)) triple13) -> (rule8 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
((((triple15) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The bear likes the tiger.
("bear" "likes" "tiger" "+")
((((((triple4) -> (rule1 % int3))) -> (rule7 % int2)) triple13) -> (rule8 % int1))
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int2
The bear is red.
("bear" "is" "red" "+")
int3
The mouse is rough.
("mouse" "is" "rough" "+")
((((((triple11) -> (rule7 % int3)) triple13) -> (rule8 % int2))) -> (rule3 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int3
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
((((((triple15) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit is rough.
("rabbit" "is" "rough" "+")
int3
The tiger is rough.
("tiger" "is" "rough" "+")
((((((((triple11) -> (rule7 % int4)) triple13) -> (rule8 % int3))) -> (rule3 % int2)) triple9) -> (rule2 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int3
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int4
The tiger is red.
("tiger" "is" "red" "+")
((((((((((triple11) -> (rule7 % int5)) triple13) -> (rule8 % int4))) -> (rule3 % int3)) triple9) -> (rule2 % int2))) -> (rule1 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int4
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int5
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
((((((((((((triple11) -> (rule7 % int6)) triple13) -> (rule8 % int5))) -> (rule3 % int4)) triple9) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger is rough.
("tiger" "is" "rough" "+")
int3
The mouse is rough.
("mouse" "is" "rough" "+")
int4
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int5
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int6
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((((((((((((((triple11) -> (rule7 % int7)) triple13) -> (rule8 % int6))) -> (rule3 % int5)) triple9) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule7 % int2)) triple13) -> (rule8 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
int3
The tiger is rough.
("tiger" "is" "rough" "+")
int4
The mouse is rough.
("mouse" "is" "rough" "+")
int5
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int6
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int7