Bob is cold. Charlie is nice. Fiona is kind. Gary is kind. Kind things are red. If Fiona is furry and Fiona is red then Fiona is quiet. Nice, furry things are cold. If something is nice then it is cold. If something is red then it is nice. Round things are kind. If something is quiet then it is kind. All round, nice things are kind.
Bob is cold.
("Bob" "is" "cold" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Kind things are red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
If Fiona is furry and Fiona is red then Fiona is quiet.
((("Fiona" "is" "furry" "+") ("Fiona" "is" "red" "+")) -> ("Fiona" "is" "quiet" "+"))
Nice, furry things are cold.
((("something" "is" "nice" "+") ("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
If something is nice then it is cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If something is red then it is nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
Round things are kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
If something is quiet then it is kind.
((("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
All round, nice things are kind.
((("something" "is" "round" "+") ("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
Gary is kind.
True
1
proof
[(triple4)]
("Gary" "is" "kind" "+")
triple4
Fiona is not kind.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "kind" "-")
triple3
Charlie is cold.
True
2
proof
[(((triple2) -> rule4))]
("Charlie" "is" "cold" "+")
((triple2) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is not cold.
False
2
inv-proof
[(((triple2) -> rule4))]
("Charlie" "is" "cold" "-")
((triple2) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Fiona is not quiet.
Unknown
inv-rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Bob is kind.
Unknown
rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "kind" "+")
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Bob is cold.[(triple1)] Charlie is nice.[(triple2)] Fiona is kind.[(triple3)] Gary is kind.[(triple4)] @1: Charlie is cold.[(((triple2) -> rule4))] Fiona is red.[(((triple3) -> rule1))] Gary is red.[(((triple4) -> rule1))] @2: Fiona is nice.[(((((triple3) -> rule1)) -> rule5))] Gary is nice.[(((((triple4) -> rule1)) -> rule5))] @3: Fiona is cold.[(((((((triple3) -> rule1)) -> rule5)) -> rule4))] Gary is cold.[(((((((triple4) -> rule1)) -> rule5)) -> rule4))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Fiona is kind.
("Fiona" "is" "kind" "+")
triple3
Gary is kind.
("Gary" "is" "kind" "+")
triple4
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple2) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((triple3) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple4) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
((((((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
((((((triple4) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3