Bob is red. Dave is rough. Erin is not green. Fiona is green. Green people are white. If someone is green and not smart then they are white. If Erin is white and Erin is smart then Erin is rough. If Fiona is white then Fiona is not quiet. If someone is red and not white then they are rough. All white, rough people are not quiet.
Bob is red.
("Bob" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is not green.
("Erin" "is" "green" "-")
Fiona is green.
("Fiona" "is" "green" "+")
Green people are white.
((("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
If someone is green and not smart then they are white.
((("someone" "is" "green" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "white" "+"))
If Erin is white and Erin is smart then Erin is rough.
((("Erin" "is" "white" "+") ("Erin" "is" "smart" "+")) -> ("Erin" "is" "rough" "+"))
If Fiona is white then Fiona is not quiet.
((("Fiona" "is" "white" "+")) -> ("Fiona" "is" "quiet" "-"))
If someone is red and not white then they are rough.
((("someone" "is" "red" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "rough" "+"))
All white, rough people are not quiet.
((("someone" "is" "white" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "-"))
Dave is rough.
True
1
proof
[(triple2)]
("Dave" "is" "rough" "+")
triple2
Erin is green.
False
1
inv-proof
[(triple3)]
("Erin" "is" "green" "+")
triple3
Fiona is white.
True
2
proof
[(((triple4) -> rule1))]
("Fiona" "is" "white" "+")
((triple4) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
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 not quiet.
True
3
proof
[(((((triple4) -> rule1)) -> rule4))]
("Fiona" "is" "quiet" "-")
((((triple4) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is quiet.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule4))]
("Fiona" "is" "quiet" "+")
((((triple4) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Erin is not rough.
Unknown
inv-rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "rough" "-")
Fiona is rough.
Unknown
rconc
[@1: Fiona is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "rough" "+")
Dave is not white.
Unknown
inv-rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "white" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Bob is red.[(triple1)] Dave is rough.[(triple2)] Erin is not green.[(triple3)] Fiona is green.[(triple4)] @1: Fiona is white.[(((triple4) -> rule1))] @2: Fiona is not quiet.[(((((triple4) -> rule1)) -> rule4))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Dave is rough.
("Dave" "is" "rough" "+")
triple2
Erin is not green.
("Erin" "is" "green" "-")
triple3
Fiona is green.
("Fiona" "is" "green" "+")
triple4
Fiona is white.
("Fiona" "is" "white" "+")
((triple4) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
((((triple4) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2