Charlie is rough. Dave is rough. All cold people are not round. If someone is big and not nice then they are not round. If someone is rough then they are not cold. If someone is furry and round then they are not cold. If Dave is not furry and Dave is not round then Dave is not quiet. If someone is rough and not cold then they are not quiet.
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is rough.
("Dave" "is" "rough" "+")
All cold people are not round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "-"))
If someone is big and not nice then they are not round.
((("someone" "is" "big" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "round" "-"))
If someone is rough then they are not cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "-"))
If someone is furry and round then they are not cold.
((("someone" "is" "furry" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "cold" "-"))
If Dave is not furry and Dave is not round then Dave is not quiet.
((("Dave" "is" "furry" "~") ("Dave" "is" "round" "~")) -> ("Dave" "is" "quiet" "-"))
If someone is rough and not cold then they are not quiet.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "quiet" "-"))
Charlie is rough.
True
1
proof
[(triple1)]
("Charlie" "is" "rough" "+")
triple1
Dave is not rough.
False
1
inv-proof
[(triple2)]
("Dave" "is" "rough" "-")
triple2
Charlie is not cold.
True
2
proof
[(((triple1) -> rule3))]
("Charlie" "is" "cold" "-")
((triple1) -> (rule3 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Charlie is cold.
False
2
inv-proof
[(((triple1) -> rule3))]
("Charlie" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Dave is not quiet.
True
4
proof
[(((triple2 ((triple2) -> rule3)) -> rule6))]
("Dave" "is" "quiet" "-")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Dave is not cold.
("Dave" "is" "cold" "-")
int2
Dave is quiet.
False
4
inv-proof
[(((triple2 ((triple2) -> rule3)) -> rule6))]
("Dave" "is" "quiet" "+")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Dave is not cold.
("Dave" "is" "cold" "-")
int2
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
Charlie is not round.
Unknown
inv-random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Charlie is rough.[(triple1)] Dave is rough.[(triple2)] @1: Charlie is not cold.[(((triple1) -> rule3))] Dave is not cold.[(((triple2) -> rule3))] @2: Charlie is not quiet.[(((triple1 ((triple1) -> rule3)) -> rule6))] Dave is not quiet.[(((triple2 ((triple2) -> rule3)) -> rule6))]
Charlie is rough.
("Charlie" "is" "rough" "+")
triple1
Dave is rough.
("Dave" "is" "rough" "+")
triple2
Charlie is not cold.
("Charlie" "is" "cold" "-")
((triple1) -> (rule3 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Dave is not cold.
("Dave" "is" "cold" "-")
((triple2) -> (rule3 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is not cold.
("Charlie" "is" "cold" "-")
int2
Dave is not quiet.
("Dave" "is" "quiet" "-")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Dave is not cold.
("Dave" "is" "cold" "-")
int2