The cat is big. The cat is green. The cat is red. The cat is rough. The cat is round. If the cat is round then the cat is red. If something is big and round then it is green. If something is green and rough then it is big. Green, big things are red. If something is big then it is red. If something is round then it is rough. All green, rough things are round. Green things are rough.
The cat is big.
("cat" "is" "big" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is round.
("cat" "is" "round" "+")
If the cat is round then the cat is red.
((("cat" "is" "round" "+")) -> ("cat" "is" "red" "+"))
If something is big and round then it is green.
((("something" "is" "big" "+") ("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
If something is green and rough then it is big.
((("something" "is" "green" "+") ("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
Green, big things are red.
((("something" "is" "green" "+") ("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
If something is big then it is red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
If something is round then it is rough.
((("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
All green, rough things are round.
((("something" "is" "green" "+") ("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
Green things are rough.
((("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
The cat is round.
True
1
proof
[(triple5 OR ((triple2 triple4) -> rule7) OR ((triple2 ((triple2) -> rule8)) -> rule7))]
("cat" "is" "round" "+")
triple5
((triple2 triple4) -> (rule7 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
((triple2 ((triple2) -> (rule8 % int2))) -> (rule7 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The cat is not red.
False
1
inv-proof
[(triple3 OR ((triple1) -> rule5) OR ((triple5) -> rule1) OR ((triple2 triple1) -> rule4) OR ((((triple2 triple4) -> rule3)) -> rule5) OR ((((triple2 triple4) -> rule7)) -> rule1) OR ((triple2 ((triple2 triple4) -> rule3)) -> rule4) OR ((((triple1 triple5) -> rule2) triple1) -> rule4) OR ((((triple1 triple5) -> rule2) ((triple2 triple4) -> rule3)) -> rule4) OR ((((triple2 ((triple2) -> rule8)) -> rule3)) -> rule5) OR ((((triple2 ((triple2) -> rule8)) -> rule7)) -> rule1) OR ((((triple2 ((triple5) -> rule6)) -> rule3)) -> rule5) OR ((triple2 ((triple2 ((triple2) -> rule8)) -> rule3)) -> rule4) OR ((triple2 ((triple2 ((triple5) -> rule6)) -> rule3)) -> rule4) OR ((((triple1 triple5) -> rule2) ((triple2 ((triple2) -> rule8)) -> rule3)) -> rule4) OR ((((triple1 triple5) -> rule2) ((triple2 ((triple5) -> rule6)) -> rule3)) -> rule4))]
("cat" "is" "red" "-")
triple3
((triple1) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
((triple5) -> (rule1 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
((triple2 triple1) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
((((triple2 triple4) -> (rule3 % int2))) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
((((triple2 triple4) -> (rule7 % int2))) -> (rule1 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
((triple2 ((triple2 triple4) -> (rule3 % int2))) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
((((triple1 triple5) -> (rule2 % int2)) triple1) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
((((triple1 triple5) -> (rule2 % int3)) ((triple2 triple4) -> (rule3 % int2))) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat is green.
("cat" "is" "green" "+")
int3
((((triple2 ((triple2) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
((((triple2 ((triple2) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
((((triple2 ((triple5) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
((triple2 ((triple2 ((triple2) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
((triple2 ((triple2 ((triple5) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
((((triple1 triple5) -> (rule2 % int4)) ((triple2 ((triple2) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
The cat is green.
("cat" "is" "green" "+")
int4
((((triple1 triple5) -> (rule2 % int4)) ((triple2 ((triple5) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
The cat is green.
("cat" "is" "green" "+")
int4
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
@0: The cat is big.[(triple1 OR ((triple2 triple4) -> rule3) OR ((triple2 ((triple2) -> rule8)) -> rule3) OR ((triple2 ((triple5) -> rule6)) -> rule3))] The cat is green.[(triple2 OR ((triple1 triple5) -> rule2))] The cat is red.[(triple3 OR ((triple1) -> rule5) OR ((triple5) -> rule1) OR ((triple2 triple1) -> rule4) OR ((((triple2 triple4) -> rule3)) -> rule5) OR ((((triple2 triple4) -> rule7)) -> rule1) OR ((triple2 ((triple2 triple4) -> rule3)) -> rule4) OR ((((triple1 triple5) -> rule2) triple1) -> rule4) OR ((((triple1 triple5) -> rule2) ((triple2 triple4) -> rule3)) -> rule4) OR ((((triple2 ((triple2) -> rule8)) -> rule3)) -> rule5) OR ((((triple2 ((triple2) -> rule8)) -> rule7)) -> rule1) OR ((((triple2 ((triple5) -> rule6)) -> rule3)) -> rule5) OR ((triple2 ((triple2 ((triple2) -> rule8)) -> rule3)) -> rule4) OR ((triple2 ((triple2 ((triple5) -> rule6)) -> rule3)) -> rule4) OR ((((triple1 triple5) -> rule2) ((triple2 ((triple2) -> rule8)) -> rule3)) -> rule4) OR ((((triple1 triple5) -> rule2) ((triple2 ((triple5) -> rule6)) -> rule3)) -> rule4))] The cat is rough.[(triple4 OR ((triple2) -> rule8) OR ((triple5) -> rule6) OR ((((triple1 triple5) -> rule2)) -> rule8))] The cat is round.[(triple5 OR ((triple2 triple4) -> rule7) OR ((triple2 ((triple2) -> rule8)) -> rule7))]
The cat is big.
("cat" "is" "big" "+")
triple1
((triple2 triple4) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
((triple2 ((triple2) -> (rule8 % int2))) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
((triple2 ((triple5) -> (rule6 % int2))) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The cat is green.
("cat" "is" "green" "+")
triple2
((triple1 triple5) -> (rule2 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is red.
("cat" "is" "red" "+")
triple3
((triple1) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
((triple5) -> (rule1 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
((triple2 triple1) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
((((triple2 triple4) -> (rule3 % int2))) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
((((triple2 triple4) -> (rule7 % int2))) -> (rule1 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
((triple2 ((triple2 triple4) -> (rule3 % int2))) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
((((triple1 triple5) -> (rule2 % int2)) triple1) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
((((triple1 triple5) -> (rule2 % int3)) ((triple2 triple4) -> (rule3 % int2))) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat is green.
("cat" "is" "green" "+")
int3
((((triple2 ((triple2) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
((((triple2 ((triple2) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
((((triple2 ((triple5) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
((triple2 ((triple2 ((triple2) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
((triple2 ((triple2 ((triple5) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
((((triple1 triple5) -> (rule2 % int4)) ((triple2 ((triple2) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
The cat is green.
("cat" "is" "green" "+")
int4
((((triple1 triple5) -> (rule2 % int4)) ((triple2 ((triple5) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
The cat is green.
("cat" "is" "green" "+")
int4
The cat is rough.
("cat" "is" "rough" "+")
triple4
((triple2) -> (rule8 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
((triple5) -> (rule6 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
((((triple1 triple5) -> (rule2 % int2))) -> (rule8 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The cat is round.
("cat" "is" "round" "+")
triple5
((triple2 triple4) -> (rule7 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
((triple2 ((triple2) -> (rule8 % int2))) -> (rule7 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2