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