Charlie is quiet. Fiona is white. Gary is big. If Gary is white and Gary is cold then Gary is red. If something is round then it is cold. Quiet things are round.
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Gary is big.
("Gary" "is" "big" "+")
If Gary is white and Gary is cold then Gary is red.
((("Gary" "is" "white" "+") ("Gary" "is" "cold" "+")) -> ("Gary" "is" "red" "+"))
If something is round then it is cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
Quiet things are round.
((("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
Charlie is quiet.
True
1
proof
[(triple1)]
("Charlie" "is" "quiet" "+")
triple1
Fiona is not white.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "white" "-")
triple2
Charlie is round.
True
2
proof
[(((triple1) -> rule3))]
("Charlie" "is" "round" "+")
((triple1) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is not round.
False
2
inv-proof
[(((triple1) -> rule3))]
("Charlie" "is" "round" "-")
((triple1) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("Charlie" "is" "cold" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is not cold.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("Charlie" "is" "cold" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Gary is not round.
Unknown
inv-rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "round" "-")
Fiona is cold.
Unknown
rconc
[@2: Fiona is cold.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Fiona" "is" "cold" "+")
Fiona is not round.
Unknown
inv-rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "round" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
@0: Charlie is quiet.[(triple1)] Fiona is white.[(triple2)] Gary is big.[(triple3)] @1: Charlie is round.[(((triple1) -> rule3))] @2: Charlie is cold.[(((((triple1) -> rule3)) -> rule2))]
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple1
Fiona is white.
("Fiona" "is" "white" "+")
triple2
Gary is big.
("Gary" "is" "big" "+")
triple3
Charlie is round.
("Charlie" "is" "round" "+")
((triple1) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2