Fiona is big. Fiona is rough. Gary is big. Gary is not furry. Gary is green. Gary is quiet. Gary is rough. All green people are white. If someone is round and not rough then they are white. If someone is white then they are round.
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is not furry.
("Gary" "is" "furry" "-")
Gary is green.
("Gary" "is" "green" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
All green people are white.
((("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
If someone is round and not rough then they are white.
((("someone" "is" "round" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "white" "+"))
If someone is white then they are round.
((("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
Gary is green.
True
1
proof
[(triple5)]
("Gary" "is" "green" "+")
triple5
Gary is not rough.
False
1
inv-proof
[(triple7)]
("Gary" "is" "rough" "-")
triple7
Gary is white.
True
2
proof
[(((triple5) -> rule1))]
("Gary" "is" "white" "+")
((triple5) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is not white.
False
2
inv-proof
[(((triple5) -> rule1))]
("Gary" "is" "white" "-")
((triple5) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is round.
True
3
proof
[(((((triple5) -> rule1)) -> rule3))]
("Gary" "is" "round" "+")
((((triple5) -> (rule1 % int2))) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is not round.
False
3
inv-proof
[(((((triple5) -> rule1)) -> rule3))]
("Gary" "is" "round" "-")
((((triple5) -> (rule1 % int2))) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Fiona is not white.
Unknown
inv-rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "white" "-")
Fiona is round.
Unknown
rconc
[@2: Fiona is round.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Fiona" "is" "round" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
@0: Fiona is big.[(triple1)] Fiona is rough.[(triple2)] Gary is big.[(triple3)] Gary is green.[(triple5)] Gary is not furry.[(triple4)] Gary is quiet.[(triple6)] Gary is rough.[(triple7)] @1: Gary is white.[(((triple5) -> rule1))] @2: Gary is round.[(((((triple5) -> rule1)) -> rule3))]
Fiona is big.
("Fiona" "is" "big" "+")
triple1
Fiona is rough.
("Fiona" "is" "rough" "+")
triple2
Gary is big.
("Gary" "is" "big" "+")
triple3
Gary is green.
("Gary" "is" "green" "+")
triple5
Gary is not furry.
("Gary" "is" "furry" "-")
triple4
Gary is quiet.
("Gary" "is" "quiet" "+")
triple6
Gary is rough.
("Gary" "is" "rough" "+")
triple7
Gary is white.
("Gary" "is" "white" "+")
((triple5) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((((triple5) -> (rule1 % int2))) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2