The cat is rough. Blue things are not round. If something is rough then it is round. If something is rough then it is round. If the cat is round and the cat is kind then the cat is nice. All blue things are kind. Round things are kind. If something is kind and not rough then it is blue. If something is round and not kind then it is not nice.
The cat is rough.
("cat" "is" "rough" "+")
Blue things are not round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "-"))
If something is rough then it is round.
((("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
If something is rough then it is round.
((("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
If the cat is round and the cat is kind then the cat is nice.
((("cat" "is" "round" "+") ("cat" "is" "kind" "+")) -> ("cat" "is" "nice" "+"))
All blue things are kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
Round things are kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
If something is kind and not rough then it is blue.
((("something" "is" "kind" "+") ("something" "is" "rough" "~")) -> ("something" "is" "blue" "+"))
If something is round and not kind then it is not nice.
((("something" "is" "round" "+") ("something" "is" "kind" "~")) -> ("something" "is" "nice" "-"))
The cat is rough.
True
1
proof
[(triple1)]
("cat" "is" "rough" "+")
triple1
The cat is not rough.
False
1
inv-proof
[(triple1)]
("cat" "is" "rough" "-")
triple1
The cat is round.
True
2
proof
[(((triple1) -> rule2) OR ((triple1) -> rule3))]
("cat" "is" "round" "+")
((triple1) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
((triple1) -> (rule3 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is not round.
False
2
inv-proof
[(((triple1) -> rule2) OR ((triple1) -> rule3))]
("cat" "is" "round" "-")
((triple1) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
((triple1) -> (rule3 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is kind.
True
3
proof
[(((((triple1) -> rule2)) -> rule6) OR ((((triple1) -> rule3)) -> rule6))]
("cat" "is" "kind" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat is not kind.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule6) OR ((((triple1) -> rule3)) -> rule6))]
("cat" "is" "kind" "-")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat is nice.
True
6
proof
[(((((triple1) -> rule2) ((((triple1) -> rule2)) -> rule6)) -> rule4) OR ((((triple1) -> rule2) ((((triple1) -> rule3)) -> rule6)) -> rule4) OR ((((triple1) -> rule3) ((((triple1) -> rule2)) -> rule6)) -> rule4) OR ((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule6)) -> rule4))]
("cat" "is" "nice" "+")
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The cat is not nice.
False
6
inv-proof
[(((((triple1) -> rule2) ((((triple1) -> rule2)) -> rule6)) -> rule4) OR ((((triple1) -> rule2) ((((triple1) -> rule3)) -> rule6)) -> rule4) OR ((((triple1) -> rule3) ((((triple1) -> rule2)) -> rule6)) -> rule4) OR ((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule6)) -> rule4))]
("cat" "is" "nice" "-")
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The cat is not blue.
Unknown
inv-rconc
[@1: The cat is blue.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "is" "blue" "-")
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 need the cat.
Unknown
inv-random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
@0: The cat is rough.[(triple1)] @1: The cat is round.[(((triple1) -> rule2) OR ((triple1) -> rule3))] @2: The cat is kind.[(((((triple1) -> rule2)) -> rule6) OR ((((triple1) -> rule3)) -> rule6))] @3: The cat is nice.[(((((triple1) -> rule2) ((((triple1) -> rule2)) -> rule6)) -> rule4) OR ((((triple1) -> rule2) ((((triple1) -> rule3)) -> rule6)) -> rule4) OR ((((triple1) -> rule3) ((((triple1) -> rule2)) -> rule6)) -> rule4) OR ((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule6)) -> rule4))]
The cat is rough.
("cat" "is" "rough" "+")
triple1
The cat is round.
("cat" "is" "round" "+")
((triple1) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
((triple1) -> (rule3 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3