The cat is green. The cat is nice. The cat is rough. All rough, kind things are not young. If something is kind and nice then it is not young. Green, nice things are young. All kind things are young. All green things are young. All young, rough things are not kind. If the cat is rough then the cat is nice. If the cat is young and the cat is green then the cat is nice.
The cat is green.
("cat" "is" "green" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is rough.
("cat" "is" "rough" "+")
All rough, kind things are not young.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "-"))
If something is kind and nice then it is not young.
((("something" "is" "kind" "+") ("something" "is" "nice" "+")) -> ("something" "is" "young" "-"))
Green, nice things are young.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
All kind things are young.
((("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
All green things are young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
All young, rough things are not kind.
((("something" "is" "young" "+") ("something" "is" "rough" "+")) -> ("something" "is" "kind" "-"))
If the cat is rough then the cat is nice.
((("cat" "is" "rough" "+")) -> ("cat" "is" "nice" "+"))
If the cat is young and the cat is green then the cat is nice.
((("cat" "is" "young" "+") ("cat" "is" "green" "+")) -> ("cat" "is" "nice" "+"))
The cat is rough.
True
1
proof
[(triple3)]
("cat" "is" "rough" "+")
triple3
The cat is not nice.
False
1
inv-proof
[(triple2 OR ((triple3) -> rule7) OR ((((triple1) -> rule5) triple1) -> rule8))]
("cat" "is" "nice" "-")
triple2
((triple3) -> (rule7 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
((((triple1) -> (rule5 % int2)) triple1) -> (rule8 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat is young.
True
2
proof
[(((triple1) -> rule5) OR ((triple1 triple2) -> rule3) OR ((triple1 ((triple3) -> rule7)) -> rule3))]
("cat" "is" "young" "+")
((triple1) -> (rule5 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
((triple1 triple2) -> (rule3 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
((triple1 ((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is not young.
False
2
inv-proof
[(((triple1) -> rule5) OR ((triple1 triple2) -> rule3) OR ((triple1 ((triple3) -> rule7)) -> rule3))]
("cat" "is" "young" "-")
((triple1) -> (rule5 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
((triple1 triple2) -> (rule3 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
((triple1 ((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is not kind.
True
4
proof
[(((((triple1) -> rule5) triple3) -> rule6) OR ((((triple1 triple2) -> rule3) triple3) -> rule6) OR ((((triple1 ((triple3) -> rule7)) -> rule3) triple3) -> rule6))]
("cat" "is" "kind" "-")
((((triple1) -> (rule5 % int2)) triple3) -> (rule6 % int1))
The cat is not kind.
("cat" "is" "kind" "-")
int1
The cat is young.
("cat" "is" "young" "+")
int2
((((triple1 triple2) -> (rule3 % int2)) triple3) -> (rule6 % int1))
The cat is not kind.
("cat" "is" "kind" "-")
int1
The cat is young.
("cat" "is" "young" "+")
int2
((((triple1 ((triple3) -> (rule7 % int3))) -> (rule3 % int2)) triple3) -> (rule6 % int1))
The cat is not kind.
("cat" "is" "kind" "-")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
The cat is kind.
False
4
inv-proof
[(((((triple1) -> rule5) triple3) -> rule6) OR ((((triple1 triple2) -> rule3) triple3) -> rule6) OR ((((triple1 ((triple3) -> rule7)) -> rule3) triple3) -> rule6))]
("cat" "is" "kind" "+")
((((triple1) -> (rule5 % int2)) triple3) -> (rule6 % int1))
The cat is not kind.
("cat" "is" "kind" "-")
int1
The cat is young.
("cat" "is" "young" "+")
int2
((((triple1 triple2) -> (rule3 % int2)) triple3) -> (rule6 % int1))
The cat is not kind.
("cat" "is" "kind" "-")
int1
The cat is young.
("cat" "is" "young" "+")
int2
((((triple1 ((triple3) -> (rule7 % int3))) -> (rule3 % int2)) triple3) -> (rule6 % int1))
The cat is not kind.
("cat" "is" "kind" "-")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
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 eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
@0: The cat is green.[(triple1)] The cat is nice.[(triple2 OR ((triple3) -> rule7) OR ((((triple1) -> rule5) triple1) -> rule8))] The cat is rough.[(triple3)] @1: The cat is young.[(((triple1) -> rule5) OR ((triple1 triple2) -> rule3) OR ((triple1 ((triple3) -> rule7)) -> rule3))] @2: The cat is not kind.[(((((triple1) -> rule5) triple3) -> rule6) OR ((((triple1 triple2) -> rule3) triple3) -> rule6) OR ((((triple1 ((triple3) -> rule7)) -> rule3) triple3) -> rule6))]
The cat is green.
("cat" "is" "green" "+")
triple1
The cat is nice.
("cat" "is" "nice" "+")
triple2
((triple3) -> (rule7 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
((((triple1) -> (rule5 % int2)) triple1) -> (rule8 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
triple3
The cat is young.
("cat" "is" "young" "+")
((triple1) -> (rule5 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
((triple1 triple2) -> (rule3 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
((triple1 ((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is not kind.
("cat" "is" "kind" "-")
((((triple1) -> (rule5 % int2)) triple3) -> (rule6 % int1))
The cat is not kind.
("cat" "is" "kind" "-")
int1
The cat is young.
("cat" "is" "young" "+")
int2
((((triple1 triple2) -> (rule3 % int2)) triple3) -> (rule6 % int1))
The cat is not kind.
("cat" "is" "kind" "-")
int1
The cat is young.
("cat" "is" "young" "+")
int2
((((triple1 ((triple3) -> (rule7 % int3))) -> (rule3 % int2)) triple3) -> (rule6 % int1))
The cat is not kind.
("cat" "is" "kind" "-")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3