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