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