The bear chases the cat. The bear needs the cat. The cat chases the bear. The cat is rough. The mouse is rough. The mouse is round. The rabbit needs the bear. If someone needs the cat then they are cold. If someone chases the rabbit and the rabbit visits the bear then the rabbit needs the mouse. If someone visits the bear then the bear visits the rabbit. If someone visits the mouse and the mouse chases the cat then the cat chases the bear. If someone chases the rabbit then the rabbit chases the mouse. If someone is cold then they chase the cat. If someone is round then they need the cat. If someone is red and they need the bear then the bear is rough.
The bear chases the cat.
("bear" "chases" "cat" "+")
The bear needs the cat.
("bear" "needs" "cat" "+")
The cat chases the bear.
("cat" "chases" "bear" "+")
The cat is rough.
("cat" "is" "rough" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is round.
("mouse" "is" "round" "+")
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
If someone needs the cat then they are cold.
((("someone" "needs" "cat" "+")) -> ("someone" "is" "cold" "+"))
If someone chases the rabbit and the rabbit visits the bear then the rabbit needs the mouse.
((("someone" "chases" "rabbit" "+") ("rabbit" "visits" "bear" "+")) -> ("rabbit" "needs" "mouse" "+"))
If someone visits the bear then the bear visits the rabbit.
((("someone" "visits" "bear" "+")) -> ("bear" "visits" "rabbit" "+"))
If someone visits the mouse and the mouse chases the cat then the cat chases the bear.
((("someone" "visits" "mouse" "+") ("mouse" "chases" "cat" "+")) -> ("cat" "chases" "bear" "+"))
If someone chases the rabbit then the rabbit chases the mouse.
((("someone" "chases" "rabbit" "+")) -> ("rabbit" "chases" "mouse" "+"))
If someone is cold then they chase the cat.
((("someone" "is" "cold" "+")) -> ("someone" "chases" "cat" "+"))
If someone is round then they need the cat.
((("someone" "is" "round" "+")) -> ("someone" "needs" "cat" "+"))
If someone is red and they need the bear then the bear is rough.
((("someone" "is" "red" "+") ("someone" "needs" "bear" "+")) -> ("bear" "is" "rough" "+"))
The cat chases the bear.
True
1
proof
[(triple3)]
("cat" "chases" "bear" "+")
triple3
The bear does not chase the cat.
False
1
inv-proof
[(triple1 OR ((((triple2) -> rule1)) -> rule6))]
("bear" "chases" "cat" "-")
triple1
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The bear chases the cat.
("bear" "chases" "cat" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The mouse needs the cat.
True
2
proof
[(((triple6) -> rule7))]
("mouse" "needs" "cat" "+")
((triple6) -> (rule7 % int1))
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int1
The mouse does not need the cat.
False
2
inv-proof
[(((triple6) -> rule7))]
("mouse" "needs" "cat" "-")
((triple6) -> (rule7 % int1))
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int1
The mouse is cold.
True
3
proof
[(((((triple6) -> rule7)) -> rule1))]
("mouse" "is" "cold" "+")
((((triple6) -> (rule7 % int2))) -> (rule1 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int2
The mouse is not cold.
False
3
inv-proof
[(((((triple6) -> rule7)) -> rule1))]
("mouse" "is" "cold" "-")
((((triple6) -> (rule7 % int2))) -> (rule1 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int2
The mouse chases the cat.
True
4
proof
[(((((((triple6) -> rule7)) -> rule1)) -> rule6))]
("mouse" "chases" "cat" "+")
((((((triple6) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int3
The mouse does not chase the cat.
False
4
inv-proof
[(((((((triple6) -> rule7)) -> rule1)) -> rule6))]
("mouse" "chases" "cat" "-")
((((((triple6) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int3
The cat does not need the cat.
Unknown
inv-rconc
[@1: The cat needs the cat.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "needs" "cat" "-")
The rabbit needs the cat.
Unknown
rconc
[@1: The rabbit needs the cat.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "needs" "cat" "+")
The rabbit is not cold.
Unknown
inv-rconc
[@2: The rabbit is cold.[CWA. Example of deepest failure = (rule1 <- rule7 <- FAIL)]]
("rabbit" "is" "cold" "-")
The bear visits the rabbit.
Unknown
rconc
[@1: The bear visits the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "visits" "rabbit" "+")
The cat does not need the bear.
Unknown
inv-random
[@0: The cat needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "bear" "-")
The rabbit chases the bear.
Unknown
random
[@0: The rabbit chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "bear" "+")
The bear is not red.
Unknown
inv-random
[@0: The bear is red.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "red" "-")
The mouse needs the rabbit.
Unknown
random
[@0: The mouse needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "rabbit" "+")
@0: The bear chases the cat.[(triple1 OR ((((triple2) -> rule1)) -> rule6))] The bear needs the cat.[(triple2)] The cat chases the bear.[(triple3)] The cat is rough.[(triple4)] The mouse is rough.[(triple5)] The mouse is round.[(triple6)] The rabbit needs the bear.[(triple7)] @1: The bear is cold.[(((triple2) -> rule1))] The mouse needs the cat.[(((triple6) -> rule7))] @2: The mouse is cold.[(((((triple6) -> rule7)) -> rule1))] @3: The mouse chases the cat.[(((((((triple6) -> rule7)) -> rule1)) -> rule6))]
The bear chases the cat.
("bear" "chases" "cat" "+")
triple1
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The bear chases the cat.
("bear" "chases" "cat" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear needs the cat.
("bear" "needs" "cat" "+")
triple2
The cat chases the bear.
("cat" "chases" "bear" "+")
triple3
The cat is rough.
("cat" "is" "rough" "+")
triple4
The mouse is rough.
("mouse" "is" "rough" "+")
triple5
The mouse is round.
("mouse" "is" "round" "+")
triple6
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
triple7
The bear is cold.
("bear" "is" "cold" "+")
((triple2) -> (rule1 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The mouse needs the cat.
("mouse" "needs" "cat" "+")
((triple6) -> (rule7 % int1))
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
((((triple6) -> (rule7 % int2))) -> (rule1 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int2
The mouse chases the cat.
("mouse" "chases" "cat" "+")
((((((triple6) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int3