Erin is cold. Fiona is rough. Gary is round. If Gary is round and Gary is big then Gary is cold. All round things are green. All green things are cold.
Erin is cold.
("Erin" "is" "cold" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
If Gary is round and Gary is big then Gary is cold.
((("Gary" "is" "round" "+") ("Gary" "is" "big" "+")) -> ("Gary" "is" "cold" "+"))
All round things are green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
All green things are cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
Fiona is rough.
True
1
proof
[(triple2)]
("Fiona" "is" "rough" "+")
triple2
Fiona is not rough.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "rough" "-")
triple2
Gary is green.
True
2
proof
[(((triple3) -> rule2))]
("Gary" "is" "green" "+")
((triple3) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is not green.
False
2
inv-proof
[(((triple3) -> rule2))]
("Gary" "is" "green" "-")
((triple3) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is cold.
True
3
proof
[(((((triple3) -> rule2)) -> rule3))]
("Gary" "is" "cold" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is not cold.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule3))]
("Gary" "is" "cold" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Fiona is not green.
Unknown
inv-rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "green" "-")
Erin is green.
Unknown
rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "green" "+")
Fiona is not cold.
Unknown
inv-rconc
[@2: Fiona is cold.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Fiona" "is" "cold" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
Erin is not big.
Unknown
inv-random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
@0: Erin is cold.[(triple1)] Fiona is rough.[(triple2)] Gary is round.[(triple3)] @1: Gary is green.[(((triple3) -> rule2))] @2: Gary is cold.[(((((triple3) -> rule2)) -> rule3))]
Erin is cold.
("Erin" "is" "cold" "+")
triple1
Fiona is rough.
("Fiona" "is" "rough" "+")
triple2
Gary is round.
("Gary" "is" "round" "+")
triple3
Gary is green.
("Gary" "is" "green" "+")
((triple3) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2