Anne is cold. Bob is not big. Charlie is cold. Gary is not cold. If Charlie is cold then Charlie is not nice. All big people are not red. If someone is cold and not nice then they are quiet.
Anne is cold.
("Anne" "is" "cold" "+")
Bob is not big.
("Bob" "is" "big" "-")
Charlie is cold.
("Charlie" "is" "cold" "+")
Gary is not cold.
("Gary" "is" "cold" "-")
If Charlie is cold then Charlie is not nice.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "nice" "-"))
All big people are not red.
((("someone" "is" "big" "+")) -> ("someone" "is" "red" "-"))
If someone is cold and not nice then they are quiet.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "quiet" "+"))
Gary is not cold.
True
1
proof
[(triple4)]
("Gary" "is" "cold" "-")
triple4
Gary is cold.
False
1
inv-proof
[(triple4)]
("Gary" "is" "cold" "+")
triple4
Charlie is not nice.
True
2
proof
[(((triple3) -> rule1))]
("Charlie" "is" "nice" "-")
((triple3) -> (rule1 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Charlie is nice.
False
2
inv-proof
[(((triple3) -> rule1))]
("Charlie" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Charlie is quiet.
True
4
proof
[(((triple3 ((triple3) -> rule1)) -> rule3))]
("Charlie" "is" "quiet" "+")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is not nice.
("Charlie" "is" "nice" "-")
int2
Charlie is not quiet.
False
4
inv-proof
[(((triple3 ((triple3) -> rule1)) -> rule3))]
("Charlie" "is" "quiet" "-")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is not nice.
("Charlie" "is" "nice" "-")
int2
Gary is not quiet.
Unknown
inv-rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "quiet" "-")
Bob is quiet.
Unknown
rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "quiet" "+")
Anne is not quiet.
Unknown
inv-rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "quiet" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
@0: Anne is cold.[(triple1)] Bob is not big.[(triple2)] Charlie is cold.[(triple3)] Gary is not cold.[(triple4)] @1: Charlie is not nice.[(((triple3) -> rule1))] @2: Charlie is quiet.[(((triple3 ((triple3) -> rule1)) -> rule3))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Bob is not big.
("Bob" "is" "big" "-")
triple2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
Gary is not cold.
("Gary" "is" "cold" "-")
triple4
Charlie is not nice.
("Charlie" "is" "nice" "-")
((triple3) -> (rule1 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is not nice.
("Charlie" "is" "nice" "-")
int2