The bear chases the cow. The bear chases the rabbit. The bear is rough. The bear likes the mouse. The cow likes the bear. The cow visits the mouse. The mouse chases the bear. The mouse chases the cow. The mouse is cold. The mouse visits the rabbit. The rabbit chases the cow. The rabbit is big. The rabbit likes the bear. The rabbit visits the cow. If someone chases the rabbit and they visit the rabbit then they like the mouse. If someone visits the mouse and they are not blue then the mouse is cold. If someone is big and they chase the bear then the bear is big. If someone is cold then they chase the bear. If someone is big then they are cold. If someone is big then they chase the mouse.
The bear chases the cow.
("bear" "chases" "cow" "+")
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear likes the mouse.
("bear" "likes" "mouse" "+")
The cow likes the bear.
("cow" "likes" "bear" "+")
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
If someone chases the rabbit and they visit the rabbit then they like the mouse.
((("someone" "chases" "rabbit" "+") ("someone" "visits" "rabbit" "+")) -> ("someone" "likes" "mouse" "+"))
If someone visits the mouse and they are not blue then the mouse is cold.
((("someone" "visits" "mouse" "+") ("someone" "is" "blue" "~")) -> ("mouse" "is" "cold" "+"))
If someone is big and they chase the bear then the bear is big.
((("someone" "is" "big" "+") ("someone" "chases" "bear" "+")) -> ("bear" "is" "big" "+"))
If someone is cold then they chase the bear.
((("someone" "is" "cold" "+")) -> ("someone" "chases" "bear" "+"))
If someone is big then they are cold.
((("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
If someone is big then they chase the mouse.
((("someone" "is" "big" "+")) -> ("someone" "chases" "mouse" "+"))
The rabbit likes the bear.
True
1
proof
[(triple13)]
("rabbit" "likes" "bear" "+")
triple13
The rabbit does not visit the cow.
False
1
inv-proof
[(triple14)]
("rabbit" "visits" "cow" "-")
triple14
The rabbit chases the mouse.
True
2
proof
[(((triple12) -> rule6))]
("rabbit" "chases" "mouse" "+")
((triple12) -> (rule6 % int1))
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int1
The rabbit does not chase the mouse.
False
2
inv-proof
[(((triple12) -> rule6))]
("rabbit" "chases" "mouse" "-")
((triple12) -> (rule6 % int1))
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int1
The rabbit chases the bear.
True
3
proof
[(((((triple12) -> rule5)) -> rule4))]
("rabbit" "chases" "bear" "+")
((((triple12) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The rabbit does not chase the bear.
False
3
inv-proof
[(((((triple12) -> rule5)) -> rule4))]
("rabbit" "chases" "bear" "-")
((((triple12) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The bear is big.
True
5
proof
[(((triple12 ((((triple12) -> rule5)) -> rule4)) -> rule3))]
("bear" "is" "big" "+")
((triple12 ((((triple12) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int2
The rabbit is cold.
("rabbit" "is" "cold" "+")
int3
The bear is not big.
False
5
inv-proof
[(((triple12 ((((triple12) -> rule5)) -> rule4)) -> rule3))]
("bear" "is" "big" "-")
((triple12 ((((triple12) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int2
The rabbit is cold.
("rabbit" "is" "cold" "+")
int3
The bear is cold.
True
6
proof
[(((((triple12 ((((triple12) -> rule5)) -> rule4)) -> rule3)) -> rule5))]
("bear" "is" "cold" "+")
((((triple12 ((((triple12) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int3
The rabbit is cold.
("rabbit" "is" "cold" "+")
int4
The bear does not chase the mouse.
False
6
inv-proof
[(((((triple12 ((((triple12) -> rule5)) -> rule4)) -> rule3)) -> rule6))]
("bear" "chases" "mouse" "-")
((((triple12 ((((triple12) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int3
The rabbit is cold.
("rabbit" "is" "cold" "+")
int4
The bear chases the bear.
True
7
proof
[(((((((triple12 ((((triple12) -> rule5)) -> rule4)) -> rule3)) -> rule5)) -> rule4))]
("bear" "chases" "bear" "+")
((((((triple12 ((((triple12) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is big.
("bear" "is" "big" "+")
int3
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int4
The rabbit is cold.
("rabbit" "is" "cold" "+")
int5
The bear does not chase the bear.
False
7
inv-proof
[(((((((triple12 ((((triple12) -> rule5)) -> rule4)) -> rule3)) -> rule5)) -> rule4))]
("bear" "chases" "bear" "-")
((((((triple12 ((((triple12) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is big.
("bear" "is" "big" "+")
int3
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int4
The rabbit is cold.
("rabbit" "is" "cold" "+")
int5
The cow does not chase the mouse.
Unknown
inv-rconc
[@1: The cow chases the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "chases" "mouse" "-")
The mouse likes the mouse.
Unknown
rconc
[@1: The mouse likes the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "likes" "mouse" "+")
The mouse does not chase the mouse.
Unknown
inv-rconc
[@1: The mouse chases the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "chases" "mouse" "-")
The cow chases the bear.
Unknown
rconc
[@2: The cow chases the bear.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("cow" "chases" "bear" "+")
The rabbit does not like the mouse.
Unknown
inv-rconc
[@1: The rabbit likes the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "likes" "mouse" "-")
The cow is cold.
Unknown
rconc
[@1: The cow is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "is" "cold" "+")
The rabbit is not blue.
Unknown
inv-random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "-")
The bear visits the cow.
Unknown
random
[@0: The bear visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "cow" "+")
The mouse does not like the cow.
Unknown
inv-random
[@0: The mouse likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "cow" "-")
The cow is blue.
Unknown
random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "+")
The bear does not like the cow.
Unknown
inv-random
[@0: The bear likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "cow" "-")
The bear likes the rabbit.
Unknown
random
[@0: The bear likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "rabbit" "+")
@0: The bear chases the cow.[(triple1)] The bear chases the rabbit.[(triple2)] The bear is rough.[(triple3)] The bear likes the mouse.[(triple4)] The cow likes the bear.[(triple5)] The cow visits the mouse.[(triple6)] The mouse chases the bear.[(triple7 OR ((triple9) -> rule4))] The mouse chases the cow.[(triple8)] The mouse is cold.[(triple9)] The mouse visits the rabbit.[(triple10)] The rabbit chases the cow.[(triple11)] The rabbit is big.[(triple12)] The rabbit likes the bear.[(triple13)] The rabbit visits the cow.[(triple14)] @1: The rabbit chases the mouse.[(((triple12) -> rule6))] The rabbit is cold.[(((triple12) -> rule5))] @2: The rabbit chases the bear.[(((((triple12) -> rule5)) -> rule4))] @3: The bear is big.[(((triple12 ((((triple12) -> rule5)) -> rule4)) -> rule3))] @4: The bear chases the mouse.[(((((triple12 ((((triple12) -> rule5)) -> rule4)) -> rule3)) -> rule6))] The bear is cold.[(((((triple12 ((((triple12) -> rule5)) -> rule4)) -> rule3)) -> rule5))] @5: The bear chases the bear.[(((((((triple12 ((((triple12) -> rule5)) -> rule4)) -> rule3)) -> rule5)) -> rule4))]
The bear chases the cow.
("bear" "chases" "cow" "+")
triple1
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
triple2
The bear is rough.
("bear" "is" "rough" "+")
triple3
The bear likes the mouse.
("bear" "likes" "mouse" "+")
triple4
The cow likes the bear.
("cow" "likes" "bear" "+")
triple5
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple6
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple7
((triple9) -> (rule4 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple8
The mouse is cold.
("mouse" "is" "cold" "+")
triple9
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple10
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
triple11
The rabbit is big.
("rabbit" "is" "big" "+")
triple12
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
triple13
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
triple14
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
((triple12) -> (rule6 % int1))
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
((triple12) -> (rule5 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
((((triple12) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The bear is big.
("bear" "is" "big" "+")
((triple12 ((((triple12) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int2
The rabbit is cold.
("rabbit" "is" "cold" "+")
int3
The bear chases the mouse.
("bear" "chases" "mouse" "+")
((((triple12 ((((triple12) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int3
The rabbit is cold.
("rabbit" "is" "cold" "+")
int4
The bear is cold.
("bear" "is" "cold" "+")
((((triple12 ((((triple12) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int3
The rabbit is cold.
("rabbit" "is" "cold" "+")
int4
The bear chases the bear.
("bear" "chases" "bear" "+")
((((((triple12 ((((triple12) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is big.
("bear" "is" "big" "+")
int3
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int4
The rabbit is cold.
("rabbit" "is" "cold" "+")
int5