Anne is red. Charlie is smart. Erin is white. Fiona is round. If someone is red and white then they are quiet. Round people are not rough. All white, smart people are not rough. All round, white people are red. If Fiona is red then Fiona is not white. If someone is white then they are round.
Anne is red.
("Anne" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is round.
("Fiona" "is" "round" "+")
If someone is red and white then they are quiet.
((("someone" "is" "red" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
Round people are not rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "-"))
All white, smart people are not rough.
((("someone" "is" "white" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "-"))
All round, white people are red.
((("someone" "is" "round" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
If Fiona is red then Fiona is not white.
((("Fiona" "is" "red" "+")) -> ("Fiona" "is" "white" "-"))
If someone is white then they are round.
((("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
Fiona is round.
True
1
proof
[(triple4)]
("Fiona" "is" "round" "+")
triple4
Fiona is not round.
False
1
inv-proof
[(triple4)]
("Fiona" "is" "round" "-")
triple4
Fiona is not rough.
True
2
proof
[(((triple4) -> rule2))]
("Fiona" "is" "rough" "-")
((triple4) -> (rule2 % int1))
Fiona is not rough.
("Fiona" "is" "rough" "-")
int1
Erin is not round.
False
2
inv-proof
[(((triple3) -> rule6))]
("Erin" "is" "round" "-")
((triple3) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is not rough.
True
3
proof
[(((((triple3) -> rule6)) -> rule2))]
("Erin" "is" "rough" "-")
((((triple3) -> (rule6 % int2))) -> (rule2 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is rough.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule2))]
("Erin" "is" "rough" "+")
((((triple3) -> (rule6 % int2))) -> (rule2 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is quiet.
True
6
proof
[(((((((triple3) -> rule6) triple3) -> rule4) triple3) -> rule1))]
("Erin" "is" "quiet" "+")
((((((triple3) -> (rule6 % int3)) triple3) -> (rule4 % int2)) triple3) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is not quiet.
False
6
inv-proof
[(((((((triple3) -> rule6) triple3) -> rule4) triple3) -> rule1))]
("Erin" "is" "quiet" "-")
((((((triple3) -> (rule6 % int3)) triple3) -> (rule4 % int2)) triple3) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Charlie is not red.
Unknown
inv-rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "red" "-")
Anne is round.
Unknown
rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "round" "+")
Fiona is not quiet.
Unknown
inv-rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Charlie is quiet.
Unknown
rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "quiet" "+")
Anne is not smart.
Unknown
inv-random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
Anne is not white.
Unknown
inv-random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
@0: Anne is red.[(triple1)] Charlie is smart.[(triple2)] Erin is white.[(triple3)] Fiona is round.[(triple4)] @1: Erin is round.[(((triple3) -> rule6))] Fiona is not rough.[(((triple4) -> rule2))] @2: Erin is not rough.[(((((triple3) -> rule6)) -> rule2))] Erin is red.[(((((triple3) -> rule6) triple3) -> rule4))] @3: Erin is quiet.[(((((((triple3) -> rule6) triple3) -> rule4) triple3) -> rule1))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple2
Erin is white.
("Erin" "is" "white" "+")
triple3
Fiona is round.
("Fiona" "is" "round" "+")
triple4
Erin is round.
("Erin" "is" "round" "+")
((triple3) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Fiona is not rough.
("Fiona" "is" "rough" "-")
((triple4) -> (rule2 % int1))
Fiona is not rough.
("Fiona" "is" "rough" "-")
int1
Erin is not rough.
("Erin" "is" "rough" "-")
((((triple3) -> (rule6 % int2))) -> (rule2 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
((((triple3) -> (rule6 % int2)) triple3) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
((((((triple3) -> (rule6 % int3)) triple3) -> (rule4 % int2)) triple3) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3