The squirrel eats the tiger. The squirrel is green. The squirrel is red. The squirrel needs the tiger. The squirrel sees the tiger. The tiger eats the squirrel. The tiger is not green. The tiger is red. The tiger does not need the squirrel. The tiger sees the squirrel. If something needs the tiger then the tiger is not nice. All cold things are kind. If something sees the squirrel and it is not nice then the squirrel is cold.
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
The tiger is not green.
("tiger" "is" "green" "-")
The tiger is red.
("tiger" "is" "red" "+")
The tiger does not need the squirrel.
("tiger" "needs" "squirrel" "-")
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
If something needs the tiger then the tiger is not nice.
((("something" "needs" "tiger" "+")) -> ("tiger" "is" "nice" "-"))
All cold things are kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
If something sees the squirrel and it is not nice then the squirrel is cold.
((("something" "sees" "squirrel" "+") ("something" "is" "nice" "~")) -> ("squirrel" "is" "cold" "+"))
The squirrel is red.
True
1
proof
[(triple3)]
("squirrel" "is" "red" "+")
triple3
The squirrel is not green.
False
1
inv-proof
[(triple2)]
("squirrel" "is" "green" "-")
triple2
The tiger is not nice.
True
2
proof
[(((triple4) -> rule1))]
("tiger" "is" "nice" "-")
((triple4) -> (rule1 % int1))
The tiger is not nice.
("tiger" "is" "nice" "-")
int1
The tiger is nice.
False
2
inv-proof
[(((triple4) -> rule1))]
("tiger" "is" "nice" "+")
((triple4) -> (rule1 % int1))
The tiger is not nice.
("tiger" "is" "nice" "-")
int1
The squirrel is cold.
True
4
proof
[(((triple10 ((triple4) -> rule1)) -> rule3))]
("squirrel" "is" "cold" "+")
((triple10 ((triple4) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The tiger is not nice.
("tiger" "is" "nice" "-")
int2
The squirrel is not cold.
False
4
inv-proof
[(((triple10 ((triple4) -> rule1)) -> rule3))]
("squirrel" "is" "cold" "-")
((triple10 ((triple4) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The tiger is not nice.
("tiger" "is" "nice" "-")
int2
The squirrel is kind.
True
5
proof
[(((((triple10 ((triple4) -> rule1)) -> rule3)) -> rule2))]
("squirrel" "is" "kind" "+")
((((triple10 ((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The tiger is not nice.
("tiger" "is" "nice" "-")
int3
The squirrel is not kind.
False
5
inv-proof
[(((((triple10 ((triple4) -> rule1)) -> rule3)) -> rule2))]
("squirrel" "is" "kind" "-")
((((triple10 ((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The tiger is not nice.
("tiger" "is" "nice" "-")
int3
The tiger is not kind.
Unknown
inv-rconc
[@1: The tiger is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "kind" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The squirrel is nice.
Unknown
random
[@0: The squirrel is nice.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "nice" "+")
The tiger is not cold.
Unknown
inv-random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
The squirrel does not eat the squirrel.
Unknown
inv-random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "-")
The squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
@0: The squirrel eats the tiger.[(triple1)] The squirrel is green.[(triple2)] The squirrel is red.[(triple3)] The squirrel needs the tiger.[(triple4)] The squirrel sees the tiger.[(triple5)] The tiger does not need the squirrel.[(triple9)] The tiger eats the squirrel.[(triple6)] The tiger is not green.[(triple7)] The tiger is red.[(triple8)] The tiger sees the squirrel.[(triple10)] @1: The tiger is not nice.[(((triple4) -> rule1))] @2: The squirrel is cold.[(((triple10 ((triple4) -> rule1)) -> rule3))] @3: The squirrel is kind.[(((((triple10 ((triple4) -> rule1)) -> rule3)) -> rule2))]
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
triple1
The squirrel is green.
("squirrel" "is" "green" "+")
triple2
The squirrel is red.
("squirrel" "is" "red" "+")
triple3
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
triple4
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
triple5
The tiger does not need the squirrel.
("tiger" "needs" "squirrel" "-")
triple9
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
triple6
The tiger is not green.
("tiger" "is" "green" "-")
triple7
The tiger is red.
("tiger" "is" "red" "+")
triple8
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
triple10
The tiger is not nice.
("tiger" "is" "nice" "-")
((triple4) -> (rule1 % int1))
The tiger is not nice.
("tiger" "is" "nice" "-")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
((triple10 ((triple4) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The tiger is not nice.
("tiger" "is" "nice" "-")
int2
The squirrel is kind.
("squirrel" "is" "kind" "+")
((((triple10 ((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The tiger is not nice.
("tiger" "is" "nice" "-")
int3