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