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