The cat is round. If something is blue and nice then it is big. If something is big and nice then it is kind. All big, blue things are kind. Round things are kind. All nice, kind things are blue. If something is kind then it is nice. Nice things are kind. If something is big then it is blue.
The cat is round.
("cat" "is" "round" "+")
If something is blue and nice then it is big.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
If something is big and nice then it is kind.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
All big, blue things are kind.
((("something" "is" "big" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
Round things are kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
All nice, kind things are blue.
((("something" "is" "nice" "+") ("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
If something is kind then it is nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
Nice things are kind.
((("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
If something is big then it is blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
The cat is round.
True
1
proof
[(triple1)]
("cat" "is" "round" "+")
triple1
The cat is not round.
False
1
inv-proof
[(triple1)]
("cat" "is" "round" "-")
triple1
The cat is kind.
True
2
proof
[(((triple1) -> rule4))]
("cat" "is" "kind" "+")
((triple1) -> (rule4 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is not kind.
False
2
inv-proof
[(((triple1) -> rule4))]
("cat" "is" "kind" "-")
((triple1) -> (rule4 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is nice.
True
3
proof
[(((((triple1) -> rule4)) -> rule6))]
("cat" "is" "nice" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is not nice.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule6))]
("cat" "is" "nice" "-")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat does not need the cat.
Unknown
inv-random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
@0: The cat is round.[(triple1)] @1: The cat is kind.[(((triple1) -> rule4))] @2: The cat is nice.[(((((triple1) -> rule4)) -> rule6))] @3: The cat is blue.[(((((((triple1) -> rule4)) -> rule6) ((triple1) -> rule4)) -> rule5))] @4: The cat is big.[(((((((((triple1) -> rule4)) -> rule6) ((triple1) -> rule4)) -> rule5) ((((triple1) -> rule4)) -> rule6)) -> rule1))]
The cat is round.
("cat" "is" "round" "+")
triple1
The cat is kind.
("cat" "is" "kind" "+")
((triple1) -> (rule4 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
((((((triple1) -> (rule4 % int3))) -> (rule6 % int2)) ((triple1) -> (rule4 % int3))) -> (rule5 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is kind.
("cat" "is" "kind" "+")
int3
The cat is big.
("cat" "is" "big" "+")
((((((((triple1) -> (rule4 % int4))) -> (rule6 % int3)) ((triple1) -> (rule4 % int4))) -> (rule5 % int2)) ((((triple1) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule1 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
The cat is kind.
("cat" "is" "kind" "+")
int4