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