The squirrel is blue. The squirrel is green. The squirrel is nice. All nice, blue things are green. All blue things are round. If something is round then it is green. Cold, green things are nice. If something is nice and round then it is blue. All green things are nice. Green things are round. Blue things are cold.
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
All nice, blue things are green.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
All blue things are round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
If something is round then it is green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
Cold, green things are nice.
((("something" "is" "cold" "+") ("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
If something is nice and round then it is blue.
((("something" "is" "nice" "+") ("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
All green things are nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
Green things are round.
((("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
Blue things are cold.
((("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
The squirrel is blue.
True
1
proof
[(triple1 OR ((triple3 ((triple2) -> rule7)) -> rule5) OR ((((triple2) -> rule6) ((triple2) -> rule7)) -> rule5))]
("squirrel" "is" "blue" "+")
triple1
((triple3 ((triple2) -> (rule7 % int2))) -> (rule5 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
((((triple2) -> (rule6 % int3)) ((triple2) -> (rule7 % int2))) -> (rule5 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
int3
The squirrel is not green.
False
1
inv-proof
[(triple2 OR ((triple3 triple1) -> rule1) OR ((((triple1) -> rule2)) -> rule3))]
("squirrel" "is" "green" "-")
triple2
((triple3 triple1) -> (rule1 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The squirrel is round.
True
2
proof
[(((triple1) -> rule2) OR ((triple2) -> rule7) OR ((((triple3 triple1) -> rule1)) -> rule7))]
("squirrel" "is" "round" "+")
((triple1) -> (rule2 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
((triple2) -> (rule7 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
((((triple3 triple1) -> (rule1 % int2))) -> (rule7 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The squirrel is not cold.
False
2
inv-proof
[(((triple1) -> rule8) OR ((((triple3 ((triple2) -> rule7)) -> rule5)) -> rule8) OR ((((((triple2) -> rule6) ((triple2) -> rule7)) -> rule5)) -> rule8))]
("squirrel" "is" "cold" "-")
((triple1) -> (rule8 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
((((triple3 ((triple2) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
int3
((((((triple2) -> (rule6 % int4)) ((triple2) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
int3
The squirrel is nice.
("squirrel" "is" "nice" "+")
int4
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 sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
@0: The squirrel is blue.[(triple1 OR ((triple3 ((triple2) -> rule7)) -> rule5) OR ((((triple2) -> rule6) ((triple2) -> rule7)) -> rule5))] The squirrel is green.[(triple2 OR ((triple3 triple1) -> rule1) OR ((((triple1) -> rule2)) -> rule3))] The squirrel is nice.[(triple3 OR ((triple2) -> rule6) OR ((((triple1) -> rule8) triple2) -> rule4) OR ((((((triple1) -> rule2)) -> rule3)) -> rule6) OR ((((triple1) -> rule8) ((((triple1) -> rule2)) -> rule3)) -> rule4))] @1: The squirrel is cold.[(((triple1) -> rule8) OR ((((triple3 ((triple2) -> rule7)) -> rule5)) -> rule8) OR ((((((triple2) -> rule6) ((triple2) -> rule7)) -> rule5)) -> rule8))] The squirrel is round.[(((triple1) -> rule2) OR ((triple2) -> rule7) OR ((((triple3 triple1) -> rule1)) -> rule7))]
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple1
((triple3 ((triple2) -> (rule7 % int2))) -> (rule5 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
((((triple2) -> (rule6 % int3)) ((triple2) -> (rule7 % int2))) -> (rule5 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
int3
The squirrel is green.
("squirrel" "is" "green" "+")
triple2
((triple3 triple1) -> (rule1 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple3
((triple2) -> (rule6 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
((((triple1) -> (rule8 % int2)) triple2) -> (rule4 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
int3
((((triple1) -> (rule8 % int4)) ((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
int3
The squirrel is cold.
("squirrel" "is" "cold" "+")
int4
The squirrel is cold.
("squirrel" "is" "cold" "+")
((triple1) -> (rule8 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
((((triple3 ((triple2) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
int3
((((((triple2) -> (rule6 % int4)) ((triple2) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
int3
The squirrel is nice.
("squirrel" "is" "nice" "+")
int4
The squirrel is round.
("squirrel" "is" "round" "+")
((triple1) -> (rule2 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
((triple2) -> (rule7 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
((((triple3 triple1) -> (rule1 % int2))) -> (rule7 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2