Charlie is not green. Erin is quiet. Fiona is not round. Gary is rough. Rough people are green. Nice people are rough. If Fiona is rough then Fiona is red. Nice, round people are not quiet. Green people are quiet. Rough people are not nice. If Charlie is nice and Charlie is quiet then Charlie is green. If someone is green and quiet then they are not round.
Charlie is not green.
("Charlie" "is" "green" "-")
Erin is quiet.
("Erin" "is" "quiet" "+")
Fiona is not round.
("Fiona" "is" "round" "-")
Gary is rough.
("Gary" "is" "rough" "+")
Rough people are green.
((("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
Nice people are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If Fiona is rough then Fiona is red.
((("Fiona" "is" "rough" "+")) -> ("Fiona" "is" "red" "+"))
Nice, round people are not quiet.
((("someone" "is" "nice" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "-"))
Green people are quiet.
((("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
Rough people are not nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "-"))
If Charlie is nice and Charlie is quiet then Charlie is green.
((("Charlie" "is" "nice" "+") ("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "green" "+"))
If someone is green and quiet then they are not round.
((("someone" "is" "green" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "-"))
Charlie is not green.
True
1
proof
[(triple1)]
("Charlie" "is" "green" "-")
triple1
Gary is not rough.
False
1
inv-proof
[(triple4)]
("Gary" "is" "rough" "-")
triple4
Gary is not nice.
True
2
proof
[(((triple4) -> rule6))]
("Gary" "is" "nice" "-")
((triple4) -> (rule6 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is nice.
False
2
inv-proof
[(((triple4) -> rule6))]
("Gary" "is" "nice" "+")
((triple4) -> (rule6 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is quiet.
True
3
proof
[(((((triple4) -> rule1)) -> rule5))]
("Gary" "is" "quiet" "+")
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is not quiet.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule5))]
("Gary" "is" "quiet" "-")
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Erin is not rough.
Unknown
inv-rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "rough" "-")
Fiona is rough.
Unknown
rconc
[@1: Fiona is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "rough" "+")
Charlie is not rough.
Unknown
inv-rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "rough" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
@0: Charlie is not green.[(triple1)] Erin is quiet.[(triple2)] Fiona is not round.[(triple3)] Gary is rough.[(triple4)] @1: Gary is green.[(((triple4) -> rule1))] Gary is not nice.[(((triple4) -> rule6))] @2: Gary is quiet.[(((((triple4) -> rule1)) -> rule5))] @3: Gary is not round.[(((((triple4) -> rule1) ((((triple4) -> rule1)) -> rule5)) -> rule8))]
Charlie is not green.
("Charlie" "is" "green" "-")
triple1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple2
Fiona is not round.
("Fiona" "is" "round" "-")
triple3
Gary is rough.
("Gary" "is" "rough" "+")
triple4
Gary is green.
("Gary" "is" "green" "+")
((triple4) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is not nice.
("Gary" "is" "nice" "-")
((triple4) -> (rule6 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is not round.
("Gary" "is" "round" "-")
((((triple4) -> (rule1 % int3)) ((((triple4) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Gary is not round.
("Gary" "is" "round" "-")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3