The cat is blue. The cat is nice. The cat is red. The cat is rough. The cat is young. Blue things are red. If something is rough then it is young. Red things are young. Young, nice things are red. All nice, young things are rough. All red things are young.
The cat is blue.
("cat" "is" "blue" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is young.
("cat" "is" "young" "+")
Blue things are red.
((("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
If something is rough then it is young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
Red things are young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
Young, nice things are red.
((("something" "is" "young" "+") ("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
All nice, young things are rough.
((("something" "is" "nice" "+") ("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
All red things are young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
The cat is young.
True
1
proof
[(triple5 OR ((triple3) -> rule3) OR ((triple3) -> rule6) OR ((triple4) -> rule2) OR ((((triple1) -> rule1)) -> rule3) OR ((((triple1) -> rule1)) -> rule6))]
("cat" "is" "young" "+")
triple5
((triple3) -> (rule3 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
((triple3) -> (rule6 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
((triple4) -> (rule2 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is not rough.
False
1
inv-proof
[(triple4 OR ((triple2 triple5) -> rule5) OR ((triple2 ((triple3) -> rule3)) -> rule5) OR ((triple2 ((triple3) -> rule6)) -> rule5) OR ((triple2 ((((triple1) -> rule1)) -> rule3)) -> rule5) OR ((triple2 ((((triple1) -> rule1)) -> rule6)) -> rule5))]
("cat" "is" "rough" "-")
triple4
((triple2 triple5) -> (rule5 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
((triple2 ((triple3) -> (rule3 % int2))) -> (rule5 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
((triple2 ((triple3) -> (rule6 % int2))) -> (rule5 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
((triple2 ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
((triple2 ((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The cat does not eat the cat.
Unknown
inv-random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
@0: The cat is blue.[(triple1)] The cat is nice.[(triple2)] The cat is red.[(triple3 OR ((triple1) -> rule1) OR ((triple5 triple2) -> rule4) OR ((((triple4) -> rule2) triple2) -> rule4))] The cat is rough.[(triple4 OR ((triple2 triple5) -> rule5) OR ((triple2 ((triple3) -> rule3)) -> rule5) OR ((triple2 ((triple3) -> rule6)) -> rule5) OR ((triple2 ((((triple1) -> rule1)) -> rule3)) -> rule5) OR ((triple2 ((((triple1) -> rule1)) -> rule6)) -> rule5))] The cat is young.[(triple5 OR ((triple3) -> rule3) OR ((triple3) -> rule6) OR ((triple4) -> rule2) OR ((((triple1) -> rule1)) -> rule3) OR ((((triple1) -> rule1)) -> rule6))]
The cat is blue.
("cat" "is" "blue" "+")
triple1
The cat is nice.
("cat" "is" "nice" "+")
triple2
The cat is red.
("cat" "is" "red" "+")
triple3
((triple1) -> (rule1 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
((triple5 triple2) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
((((triple4) -> (rule2 % int2)) triple2) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
triple4
((triple2 triple5) -> (rule5 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
((triple2 ((triple3) -> (rule3 % int2))) -> (rule5 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
((triple2 ((triple3) -> (rule6 % int2))) -> (rule5 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
((triple2 ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
((triple2 ((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The cat is young.
("cat" "is" "young" "+")
triple5
((triple3) -> (rule3 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
((triple3) -> (rule6 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
((triple4) -> (rule2 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2