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