The cat is big. The cat is nice. The cat is red. All nice things are big. If something is big then it is green. All green things are big. If the cat is big and the cat is green then the cat is nice. If something is big and nice then it is red. All young, green things are big.
The cat is big.
("cat" "is" "big" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is red.
("cat" "is" "red" "+")
All nice things are big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
If something is big then it is green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
All green things are big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
If the cat is big and the cat is green then the cat is nice.
((("cat" "is" "big" "+") ("cat" "is" "green" "+")) -> ("cat" "is" "nice" "+"))
If something is big and nice then it is red.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
All young, green things are big.
((("something" "is" "young" "+") ("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
The cat is big.
True
1
proof
[(triple1 OR ((triple2) -> rule1))]
("cat" "is" "big" "+")
triple1
((triple2) -> (rule1 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is not red.
False
1
inv-proof
[(triple3 OR ((triple1 triple2) -> rule5) OR ((((triple2) -> rule1) triple2) -> rule5) OR ((triple1 ((triple1 ((triple1) -> rule2)) -> rule4)) -> rule5) OR ((((triple2) -> rule1) ((triple1 ((triple1) -> rule2)) -> rule4)) -> rule5))]
("cat" "is" "red" "-")
triple3
((triple1 triple2) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
((((triple2) -> (rule1 % int2)) triple2) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
((triple1 ((triple1 ((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is green.
("cat" "is" "green" "+")
int3
((((triple2) -> (rule1 % int4)) ((triple1 ((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is green.
("cat" "is" "green" "+")
int3
The cat is big.
("cat" "is" "big" "+")
int4
The cat is green.
True
2
proof
[(((triple1) -> rule2) OR ((((triple2) -> rule1)) -> rule2))]
("cat" "is" "green" "+")
((triple1) -> (rule2 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat is not green.
False
2
inv-proof
[(((triple1) -> rule2) OR ((((triple2) -> rule1)) -> rule2))]
("cat" "is" "green" "-")
((triple1) -> (rule2 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
The cat does not chase the cat.
Unknown
inv-random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "-")
The cat is young.
Unknown
random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "+")
@0: The cat is big.[(triple1 OR ((triple2) -> rule1))] The cat is nice.[(triple2 OR ((triple1 ((triple1) -> rule2)) -> rule4))] The cat is red.[(triple3 OR ((triple1 triple2) -> rule5) OR ((((triple2) -> rule1) triple2) -> rule5) OR ((triple1 ((triple1 ((triple1) -> rule2)) -> rule4)) -> rule5) OR ((((triple2) -> rule1) ((triple1 ((triple1) -> rule2)) -> rule4)) -> rule5))] @1: The cat is green.[(((triple1) -> rule2) OR ((((triple2) -> rule1)) -> rule2))]
The cat is big.
("cat" "is" "big" "+")
triple1
((triple2) -> (rule1 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
triple2
((triple1 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The cat is red.
("cat" "is" "red" "+")
triple3
((triple1 triple2) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
((((triple2) -> (rule1 % int2)) triple2) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
((triple1 ((triple1 ((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is green.
("cat" "is" "green" "+")
int3
((((triple2) -> (rule1 % int4)) ((triple1 ((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is green.
("cat" "is" "green" "+")
int3
The cat is big.
("cat" "is" "big" "+")
int4
The cat is green.
("cat" "is" "green" "+")
((triple1) -> (rule2 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2