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