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