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