The squirrel is big. The squirrel is blue. The squirrel is cold. The squirrel is nice. The squirrel is round. All round things are cold. If the squirrel is blue and the squirrel is nice then the squirrel is big. If something is cold then it is nice. All big things are nice. Cold things are nice. If something is big and not cold then it is nice.
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
All round things are cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
If the squirrel is blue and the squirrel is nice then the squirrel is big.
((("squirrel" "is" "blue" "+") ("squirrel" "is" "nice" "+")) -> ("squirrel" "is" "big" "+"))
If something is cold then it is nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
All big things are nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
Cold things are nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If something is big and not cold then it is nice.
((("something" "is" "big" "+") ("something" "is" "cold" "~")) -> ("something" "is" "nice" "+"))
The squirrel is nice.
True
1
proof
[(triple4 OR ((triple1) -> rule4) OR ((triple3) -> rule3) OR ((triple3) -> rule5) OR ((((triple5) -> rule1)) -> rule3) OR ((((triple5) -> rule1)) -> rule5))]
("squirrel" "is" "nice" "+")
triple4
((triple1) -> (rule4 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
((triple3) -> (rule3 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
((triple3) -> (rule5 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
((((triple5) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
((((triple5) -> (rule1 % int2))) -> (rule5 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The squirrel is not nice.
False
1
inv-proof
[(triple4 OR ((triple1) -> rule4) OR ((triple3) -> rule3) OR ((triple3) -> rule5) OR ((((triple5) -> rule1)) -> rule3) OR ((((triple5) -> rule1)) -> rule5))]
("squirrel" "is" "nice" "-")
triple4
((triple1) -> (rule4 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
((triple3) -> (rule3 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
((triple3) -> (rule5 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
((((triple5) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
((((triple5) -> (rule1 % int2))) -> (rule5 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The squirrel does not like the squirrel.
Unknown
inv-random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "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 is big.[(triple1 OR ((triple2 triple4) -> rule2) OR ((triple2 ((triple3) -> rule3)) -> rule2) OR ((triple2 ((triple3) -> rule5)) -> rule2) OR ((triple2 ((((triple5) -> rule1)) -> rule3)) -> rule2) OR ((triple2 ((((triple5) -> rule1)) -> rule5)) -> rule2))] The squirrel is blue.[(triple2)] The squirrel is cold.[(triple3 OR ((triple5) -> rule1))] The squirrel is nice.[(triple4 OR ((triple1) -> rule4) OR ((triple3) -> rule3) OR ((triple3) -> rule5) OR ((((triple5) -> rule1)) -> rule3) OR ((((triple5) -> rule1)) -> rule5))] The squirrel is round.[(triple5)]
The squirrel is big.
("squirrel" "is" "big" "+")
triple1
((triple2 triple4) -> (rule2 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
((triple2 ((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
((triple2 ((triple3) -> (rule5 % int2))) -> (rule2 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
((triple2 ((((triple5) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
((triple2 ((((triple5) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple2
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple3
((triple5) -> (rule1 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple4
((triple1) -> (rule4 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
((triple3) -> (rule3 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
((triple3) -> (rule5 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
((((triple5) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
((((triple5) -> (rule1 % int2))) -> (rule5 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
triple5