The cat is kind. The cat is not nice. The cat is rough. All nice people are cold. Nice people are not rough. If someone is young then they are rough. If someone is cold and not nice then they are rough. Nice people are not kind. If the cat is rough and the cat is not nice then the cat is cold. If the cat is kind then the cat is cold. All cold, rough people are young.
The cat is kind.
("cat" "is" "kind" "+")
The cat is not nice.
("cat" "is" "nice" "-")
The cat is rough.
("cat" "is" "rough" "+")
All nice people are cold.
((("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
Nice people are not rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "-"))
If someone is young then they are rough.
((("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
If someone is cold and not nice then they are rough.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "rough" "+"))
Nice people are not kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "-"))
If the cat is rough and the cat is not nice then the cat is cold.
((("cat" "is" "rough" "+") ("cat" "is" "nice" "~")) -> ("cat" "is" "cold" "+"))
If the cat is kind then the cat is cold.
((("cat" "is" "kind" "+")) -> ("cat" "is" "cold" "+"))
All cold, rough people are young.
((("someone" "is" "cold" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
The cat is kind.
True
1
proof
[(triple1)]
("cat" "is" "kind" "+")
triple1
The cat is not rough.
False
1
inv-proof
[(triple3 OR ((((triple1) -> rule7) triple2) -> rule4))]
("cat" "is" "rough" "-")
triple3
((((triple1) -> (rule7 % int2)) triple2) -> (rule4 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat is cold.
True
2
proof
[(((triple1) -> rule7) OR ((triple3 triple2) -> rule6))]
("cat" "is" "cold" "+")
((triple1) -> (rule7 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
((triple3 triple2) -> (rule6 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is not cold.
False
2
inv-proof
[(((triple1) -> rule7) OR ((triple3 triple2) -> rule6))]
("cat" "is" "cold" "-")
((triple1) -> (rule7 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
((triple3 triple2) -> (rule6 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is young.
True
4
proof
[(((((triple1) -> rule7) triple3) -> rule8) OR ((((triple3 triple2) -> rule6) triple3) -> rule8) OR ((((triple1) -> rule7) ((((triple1) -> rule7) triple2) -> rule4)) -> rule8) OR ((((triple3 triple2) -> rule6) ((((triple1) -> rule7) triple2) -> rule4)) -> rule8))]
("cat" "is" "young" "+")
((((triple1) -> (rule7 % int2)) triple3) -> (rule8 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
((((triple3 triple2) -> (rule6 % int2)) triple3) -> (rule8 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
((((triple1) -> (rule7 % int3)) ((((triple1) -> (rule7 % int3)) triple2) -> (rule4 % int2))) -> (rule8 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3
((((triple3 triple2) -> (rule6 % int3)) ((((triple1) -> (rule7 % int3)) triple2) -> (rule4 % int2))) -> (rule8 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3
The cat is not young.
False
4
inv-proof
[(((((triple1) -> rule7) triple3) -> rule8) OR ((((triple3 triple2) -> rule6) triple3) -> rule8) OR ((((triple1) -> rule7) ((((triple1) -> rule7) triple2) -> rule4)) -> rule8) OR ((((triple3 triple2) -> rule6) ((((triple1) -> rule7) triple2) -> rule4)) -> rule8))]
("cat" "is" "young" "-")
((((triple1) -> (rule7 % int2)) triple3) -> (rule8 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
((((triple3 triple2) -> (rule6 % int2)) triple3) -> (rule8 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
((((triple1) -> (rule7 % int3)) ((((triple1) -> (rule7 % int3)) triple2) -> (rule4 % int2))) -> (rule8 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3
((((triple3 triple2) -> (rule6 % int3)) ((((triple1) -> (rule7 % int3)) triple2) -> (rule4 % int2))) -> (rule8 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3
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 chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
@0: The cat is kind.[(triple1)] The cat is not nice.[(triple2)] The cat is rough.[(triple3 OR ((((triple1) -> rule7) triple2) -> rule4))] @1: The cat is cold.[(((triple1) -> rule7) OR ((triple3 triple2) -> rule6))] @2: The cat is young.[(((((triple1) -> rule7) triple3) -> rule8) OR ((((triple3 triple2) -> rule6) triple3) -> rule8) OR ((((triple1) -> rule7) ((((triple1) -> rule7) triple2) -> rule4)) -> rule8) OR ((((triple3 triple2) -> rule6) ((((triple1) -> rule7) triple2) -> rule4)) -> rule8))]
The cat is kind.
("cat" "is" "kind" "+")
triple1
The cat is not nice.
("cat" "is" "nice" "-")
triple2
The cat is rough.
("cat" "is" "rough" "+")
triple3
((((triple1) -> (rule7 % int2)) triple2) -> (rule4 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
((triple1) -> (rule7 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
((triple3 triple2) -> (rule6 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is young.
("cat" "is" "young" "+")
((((triple1) -> (rule7 % int2)) triple3) -> (rule8 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
((((triple3 triple2) -> (rule6 % int2)) triple3) -> (rule8 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
((((triple1) -> (rule7 % int3)) ((((triple1) -> (rule7 % int3)) triple2) -> (rule4 % int2))) -> (rule8 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3
((((triple3 triple2) -> (rule6 % int3)) ((((triple1) -> (rule7 % int3)) triple2) -> (rule4 % int2))) -> (rule8 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3