Anne is white. Charlie is red. Fiona is kind. Gary is round. If someone is round then they are rough. All rough, kind people are red. Cold people are red. If Fiona is furry and Fiona is cold then Fiona is rough. If Anne is rough then Anne is red. Rough, round people are white. All white, rough people are cold. If Gary is furry then Gary is round.
Anne is white.
("Anne" "is" "white" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Gary is round.
("Gary" "is" "round" "+")
If someone is round then they are rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
All rough, kind people are red.
((("someone" "is" "rough" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
Cold people are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
If Fiona is furry and Fiona is cold then Fiona is rough.
((("Fiona" "is" "furry" "+") ("Fiona" "is" "cold" "+")) -> ("Fiona" "is" "rough" "+"))
If Anne is rough then Anne is red.
((("Anne" "is" "rough" "+")) -> ("Anne" "is" "red" "+"))
Rough, round people are white.
((("someone" "is" "rough" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
All white, rough people are cold.
((("someone" "is" "white" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
If Gary is furry then Gary is round.
((("Gary" "is" "furry" "+")) -> ("Gary" "is" "round" "+"))
Charlie is red.
True
1
proof
[(triple2)]
("Charlie" "is" "red" "+")
triple2
Gary is not round.
False
1
inv-proof
[(triple4)]
("Gary" "is" "round" "-")
triple4
Gary is rough.
True
2
proof
[(((triple4) -> rule1))]
("Gary" "is" "rough" "+")
((triple4) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is not rough.
False
2
inv-proof
[(((triple4) -> rule1))]
("Gary" "is" "rough" "-")
((triple4) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is white.
True
4
proof
[(((((triple4) -> rule1) triple4) -> rule6))]
("Gary" "is" "white" "+")
((((triple4) -> (rule1 % int2)) triple4) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is not white.
False
4
inv-proof
[(((((triple4) -> rule1) triple4) -> rule6))]
("Gary" "is" "white" "-")
((((triple4) -> (rule1 % int2)) triple4) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is cold.
True
7
proof
[(((((((triple4) -> rule1) triple4) -> rule6) ((triple4) -> rule1)) -> rule7))]
("Gary" "is" "cold" "+")
((((((triple4) -> (rule1 % int3)) triple4) -> (rule6 % int2)) ((triple4) -> (rule1 % int3))) -> (rule7 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is not cold.
False
7
inv-proof
[(((((((triple4) -> rule1) triple4) -> rule6) ((triple4) -> rule1)) -> rule7))]
("Gary" "is" "cold" "-")
((((((triple4) -> (rule1 % int3)) triple4) -> (rule6 % int2)) ((triple4) -> (rule1 % int3))) -> (rule7 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Anne is not rough.
Unknown
inv-rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "rough" "-")
Fiona is rough.
Unknown
rconc
[@1: Fiona is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "rough" "+")
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "white" "-")
Anne is cold.
Unknown
rconc
[@2: Anne is cold.[CWA. Example of deepest failure = (rule7 <- rule1 <- FAIL)]]
("Anne" "is" "cold" "+")
Charlie is not round.
Unknown
inv-random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Anne is white.[(triple1)] Charlie is red.[(triple2)] Fiona is kind.[(triple3)] Gary is round.[(triple4)] @1: Gary is rough.[(((triple4) -> rule1))] @2: Gary is white.[(((((triple4) -> rule1) triple4) -> rule6))] @3: Gary is cold.[(((((((triple4) -> rule1) triple4) -> rule6) ((triple4) -> rule1)) -> rule7))] @4: Gary is red.[(((((((((triple4) -> rule1) triple4) -> rule6) ((triple4) -> rule1)) -> rule7)) -> rule3))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Fiona is kind.
("Fiona" "is" "kind" "+")
triple3
Gary is round.
("Gary" "is" "round" "+")
triple4
Gary is rough.
("Gary" "is" "rough" "+")
((triple4) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((((triple4) -> (rule1 % int2)) triple4) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((((((triple4) -> (rule1 % int3)) triple4) -> (rule6 % int2)) ((triple4) -> (rule1 % int3))) -> (rule7 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
((((((((triple4) -> (rule1 % int4)) triple4) -> (rule6 % int3)) ((triple4) -> (rule1 % int4))) -> (rule7 % int2))) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4