The dog is big. The dog needs the rabbit. The dog does not see the mouse. The dog visits the mouse. The dog visits the rabbit. The mouse is big. The mouse is blue. The mouse is cold. The mouse is rough. The mouse needs the rabbit. The mouse sees the rabbit. The mouse visits the dog. The rabbit is red. The rabbit visits the dog. The rabbit visits the mouse. If someone sees the rabbit and the rabbit visits the mouse then the rabbit is rough. If someone is rough and they visit the dog then they see the rabbit. If someone visits the dog then the dog is rough. If someone is blue and they visit the dog then the dog needs the rabbit. If someone is rough then they do not need the dog. If someone visits the dog then they do not see the mouse. If someone is big and they do not need the dog then they are cold. If someone sees the dog and they do not see the rabbit then they do not need the rabbit.
The dog is big.
("dog" "is" "big" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The dog does not see the mouse.
("dog" "sees" "mouse" "-")
The dog visits the mouse.
("dog" "visits" "mouse" "+")
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
If someone sees the rabbit and the rabbit visits the mouse then the rabbit is rough.
((("someone" "sees" "rabbit" "+") ("rabbit" "visits" "mouse" "+")) -> ("rabbit" "is" "rough" "+"))
If someone is rough and they visit the dog then they see the rabbit.
((("someone" "is" "rough" "+") ("someone" "visits" "dog" "+")) -> ("someone" "sees" "rabbit" "+"))
If someone visits the dog then the dog is rough.
((("someone" "visits" "dog" "+")) -> ("dog" "is" "rough" "+"))
If someone is blue and they visit the dog then the dog needs the rabbit.
((("someone" "is" "blue" "+") ("someone" "visits" "dog" "+")) -> ("dog" "needs" "rabbit" "+"))
If someone is rough then they do not need the dog.
((("someone" "is" "rough" "+")) -> ("someone" "needs" "dog" "-"))
If someone visits the dog then they do not see the mouse.
((("someone" "visits" "dog" "+")) -> ("someone" "sees" "mouse" "-"))
If someone is big and they do not need the dog then they are cold.
((("someone" "is" "big" "+") ("someone" "needs" "dog" "~")) -> ("someone" "is" "cold" "+"))
If someone sees the dog and they do not see the rabbit then they do not need the rabbit.
((("someone" "sees" "dog" "+") ("someone" "sees" "rabbit" "~")) -> ("someone" "needs" "rabbit" "-"))
The rabbit visits the dog.
True
1
proof
[(triple14)]
("rabbit" "visits" "dog" "+")
triple14
The mouse is not rough.
False
1
inv-proof
[(triple9)]
("mouse" "is" "rough" "-")
triple9
The dog is rough.
True
2
proof
[(((triple12) -> rule3) OR ((triple14) -> rule3))]
("dog" "is" "rough" "+")
((triple12) -> (rule3 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
((triple14) -> (rule3 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The rabbit sees the mouse.
False
2
inv-proof
[(((triple14) -> rule6))]
("rabbit" "sees" "mouse" "+")
((triple14) -> (rule6 % int1))
The rabbit does not see the mouse.
("rabbit" "sees" "mouse" "-")
int1
The rabbit sees the rabbit.
True
5
proof
[(((((triple11 triple15) -> rule1) triple14) -> rule2) OR ((((((triple9 triple12) -> rule2) triple15) -> rule1) triple14) -> rule2))]
("rabbit" "sees" "rabbit" "+")
((((triple11 triple15) -> (rule1 % int2)) triple14) -> (rule2 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
((((((triple9 triple12) -> (rule2 % int3)) triple15) -> (rule1 % int2)) triple14) -> (rule2 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int3
The dog needs the dog.
False
3
inv-proof
[(((((triple12) -> rule3)) -> rule5) OR ((((triple14) -> rule3)) -> rule5))]
("dog" "needs" "dog" "+")
((((triple12) -> (rule3 % int2))) -> (rule5 % int1))
The dog does not need the dog.
("dog" "needs" "dog" "-")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
((((triple14) -> (rule3 % int2))) -> (rule5 % int1))
The dog does not need the dog.
("dog" "needs" "dog" "-")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
The dog is cold.
True
5
proof
[(((triple1 ((((triple12) -> rule3)) -> rule5)) -> rule7) OR ((triple1 ((((triple14) -> rule3)) -> rule5)) -> rule7))]
("dog" "is" "cold" "+")
((triple1 ((((triple12) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog does not need the dog.
("dog" "needs" "dog" "-")
int2
The dog is rough.
("dog" "is" "rough" "+")
int3
((triple1 ((((triple14) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog does not need the dog.
("dog" "needs" "dog" "-")
int2
The dog is rough.
("dog" "is" "rough" "+")
int3
The dog is not cold.
False
5
inv-proof
[(((triple1 ((((triple12) -> rule3)) -> rule5)) -> rule7) OR ((triple1 ((((triple14) -> rule3)) -> rule5)) -> rule7))]
("dog" "is" "cold" "-")
((triple1 ((((triple12) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog does not need the dog.
("dog" "needs" "dog" "-")
int2
The dog is rough.
("dog" "is" "rough" "+")
int3
((triple1 ((((triple14) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog does not need the dog.
("dog" "needs" "dog" "-")
int2
The dog is rough.
("dog" "is" "rough" "+")
int3
The dog does not see the rabbit.
Unknown
inv-rconc
[@1: The dog sees the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "sees" "rabbit" "-")
The rabbit is cold.
Unknown
rconc
[@1: The rabbit is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "is" "cold" "+")
The mouse does not see the dog.
Unknown
inv-random
[@0: The mouse sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "dog" "-")
The mouse visits the rabbit.
Unknown
random
[@0: The mouse visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "rabbit" "+")
The rabbit is not blue.
Unknown
inv-random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "-")
The dog needs the mouse.
Unknown
random
[@0: The dog needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "mouse" "+")
The dog is not blue.
Unknown
inv-random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
@0: The dog does not see the mouse.[(triple3)] The dog is big.[(triple1)] The dog needs the rabbit.[(triple2 OR ((triple7 triple12) -> rule4))] The dog visits the mouse.[(triple4)] The dog visits the rabbit.[(triple5)] The mouse is big.[(triple6)] The mouse is blue.[(triple7)] The mouse is cold.[(triple8 OR ((triple6 ((triple9) -> rule5)) -> rule7))] The mouse is rough.[(triple9)] The mouse needs the rabbit.[(triple10)] The mouse sees the rabbit.[(triple11 OR ((triple9 triple12) -> rule2))] The mouse visits the dog.[(triple12)] The rabbit is red.[(triple13)] The rabbit visits the dog.[(triple14)] The rabbit visits the mouse.[(triple15)] @1: The dog is rough.[(((triple12) -> rule3) OR ((triple14) -> rule3))] The mouse does not need the dog.[(((triple9) -> rule5))] The mouse does not see the mouse.[(((triple12) -> rule6))] The rabbit does not see the mouse.[(((triple14) -> rule6))] The rabbit is rough.[(((triple11 triple15) -> rule1) OR ((((triple9 triple12) -> rule2) triple15) -> rule1))] @2: The dog does not need the dog.[(((((triple12) -> rule3)) -> rule5) OR ((((triple14) -> rule3)) -> rule5))] The rabbit does not need the dog.[(((((triple11 triple15) -> rule1)) -> rule5) OR ((((((triple9 triple12) -> rule2) triple15) -> rule1)) -> rule5))] The rabbit sees the rabbit.[(((((triple11 triple15) -> rule1) triple14) -> rule2) OR ((((((triple9 triple12) -> rule2) triple15) -> rule1) triple14) -> rule2))] @3: The dog is cold.[(((triple1 ((((triple12) -> rule3)) -> rule5)) -> rule7) OR ((triple1 ((((triple14) -> rule3)) -> rule5)) -> rule7))]
The dog does not see the mouse.
("dog" "sees" "mouse" "-")
triple3
The dog is big.
("dog" "is" "big" "+")
triple1
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple2
((triple7 triple12) -> (rule4 % int1))
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int1
The dog visits the mouse.
("dog" "visits" "mouse" "+")
triple4
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
triple5
The mouse is big.
("mouse" "is" "big" "+")
triple6
The mouse is blue.
("mouse" "is" "blue" "+")
triple7
The mouse is cold.
("mouse" "is" "cold" "+")
triple8
((triple6 ((triple9) -> (rule5 % int2))) -> (rule7 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse does not need the dog.
("mouse" "needs" "dog" "-")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
triple9
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple10
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple11
((triple9 triple12) -> (rule2 % int1))
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int1
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple12
The rabbit is red.
("rabbit" "is" "red" "+")
triple13
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
triple14
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple15
The dog is rough.
("dog" "is" "rough" "+")
((triple12) -> (rule3 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
((triple14) -> (rule3 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The mouse does not need the dog.
("mouse" "needs" "dog" "-")
((triple9) -> (rule5 % int1))
The mouse does not need the dog.
("mouse" "needs" "dog" "-")
int1
The mouse does not see the mouse.
("mouse" "sees" "mouse" "-")
((triple12) -> (rule6 % int1))
The mouse does not see the mouse.
("mouse" "sees" "mouse" "-")
int1
The rabbit does not see the mouse.
("rabbit" "sees" "mouse" "-")
((triple14) -> (rule6 % int1))
The rabbit does not see the mouse.
("rabbit" "sees" "mouse" "-")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
((triple11 triple15) -> (rule1 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
((((triple9 triple12) -> (rule2 % int2)) triple15) -> (rule1 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int2
The dog does not need the dog.
("dog" "needs" "dog" "-")
((((triple12) -> (rule3 % int2))) -> (rule5 % int1))
The dog does not need the dog.
("dog" "needs" "dog" "-")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
((((triple14) -> (rule3 % int2))) -> (rule5 % int1))
The dog does not need the dog.
("dog" "needs" "dog" "-")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
The rabbit does not need the dog.
("rabbit" "needs" "dog" "-")
((((triple11 triple15) -> (rule1 % int2))) -> (rule5 % int1))
The rabbit does not need the dog.
("rabbit" "needs" "dog" "-")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
((((((triple9 triple12) -> (rule2 % int3)) triple15) -> (rule1 % int2))) -> (rule5 % int1))
The rabbit does not need the dog.
("rabbit" "needs" "dog" "-")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int3
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((((triple11 triple15) -> (rule1 % int2)) triple14) -> (rule2 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
((((((triple9 triple12) -> (rule2 % int3)) triple15) -> (rule1 % int2)) triple14) -> (rule2 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int3
The dog is cold.
("dog" "is" "cold" "+")
((triple1 ((((triple12) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog does not need the dog.
("dog" "needs" "dog" "-")
int2
The dog is rough.
("dog" "is" "rough" "+")
int3
((triple1 ((((triple14) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog does not need the dog.
("dog" "needs" "dog" "-")
int2
The dog is rough.
("dog" "is" "rough" "+")
int3