Charlie is smart. Fiona is smart. Gary is white. If Charlie is cold and Charlie is rough then Charlie is white. Cold, kind things are round. Cold things are rough. Rough, kind things are smart. If Gary is white and Gary is blue then Gary is smart. If Fiona is white then Fiona is round. Round things are white. If something is smart then it is cold.
Charlie is smart.
("Charlie" "is" "smart" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
If Charlie is cold and Charlie is rough then Charlie is white.
((("Charlie" "is" "cold" "+") ("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "white" "+"))
Cold, kind things are round.
((("something" "is" "cold" "+") ("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
Cold things are rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
Rough, kind things are smart.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
If Gary is white and Gary is blue then Gary is smart.
((("Gary" "is" "white" "+") ("Gary" "is" "blue" "+")) -> ("Gary" "is" "smart" "+"))
If Fiona is white then Fiona is round.
((("Fiona" "is" "white" "+")) -> ("Fiona" "is" "round" "+"))
Round things are white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
If something is smart then it is cold.
((("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
Charlie is smart.
True
1
proof
[(triple1)]
("Charlie" "is" "smart" "+")
triple1
Fiona is not smart.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "smart" "-")
triple2
Fiona is cold.
True
2
proof
[(((triple2) -> rule8))]
("Fiona" "is" "cold" "+")
((triple2) -> (rule8 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Charlie is not cold.
False
2
inv-proof
[(((triple1) -> rule8))]
("Charlie" "is" "cold" "-")
((triple1) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Fiona is rough.
True
3
proof
[(((((triple2) -> rule8)) -> rule3))]
("Fiona" "is" "rough" "+")
((((triple2) -> (rule8 % int2))) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is not rough.
False
3
inv-proof
[(((((triple2) -> rule8)) -> rule3))]
("Fiona" "is" "rough" "-")
((((triple2) -> (rule8 % int2))) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Gary is not round.
Unknown
inv-rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "round" "-")
Charlie is round.
Unknown
rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "round" "+")
Fiona is not round.
Unknown
inv-rconc
[@3: Fiona is round.[CWA. Example of deepest failure = (rule6 <- rule7 <- rule2 <- FAIL)]]
("Fiona" "is" "round" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
@0: Charlie is smart.[(triple1)] Fiona is smart.[(triple2)] Gary is white.[(triple3)] @1: Charlie is cold.[(((triple1) -> rule8))] Fiona is cold.[(((triple2) -> rule8))] @2: Charlie is rough.[(((((triple1) -> rule8)) -> rule3))] Fiona is rough.[(((((triple2) -> rule8)) -> rule3))] @3: Charlie is white.[(((((triple1) -> rule8) ((((triple1) -> rule8)) -> rule3)) -> rule1))]
Charlie is smart.
("Charlie" "is" "smart" "+")
triple1
Fiona is smart.
("Fiona" "is" "smart" "+")
triple2
Gary is white.
("Gary" "is" "white" "+")
triple3
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple1) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple2) -> (rule8 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple1) -> (rule8 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
((((triple2) -> (rule8 % int2))) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((((triple1) -> (rule8 % int3)) ((((triple1) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3