Dave is blue. Dave is nice. Dave is white. Fiona is kind. Gary is blue. Gary is nice. Harry is cold. All kind things are white. Cold things are furry. All blue, young things are furry. All blue things are cold. If something is furry then it is white. Nice things are kind.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Harry is cold.
("Harry" "is" "cold" "+")
All kind things are white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
Cold things are furry.
((("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
All blue, young things are furry.
((("something" "is" "blue" "+") ("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
All blue things are cold.
((("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
If something is furry then it is white.
((("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
Nice things are kind.
((("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
Harry is cold.
True
1
proof
[(triple7)]
("Harry" "is" "cold" "+")
triple7
Harry is not cold.
False
1
inv-proof
[(triple7)]
("Harry" "is" "cold" "-")
triple7
Dave is cold.
True
2
proof
[(((triple1) -> rule4))]
("Dave" "is" "cold" "+")
((triple1) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is not kind.
False
2
inv-proof
[(((triple2) -> rule6))]
("Dave" "is" "kind" "-")
((triple2) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Harry is white.
True
3
proof
[(((((triple7) -> rule2)) -> rule5))]
("Harry" "is" "white" "+")
((((triple7) -> (rule2 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Gary is not furry.
False
3
inv-proof
[(((((triple5) -> rule4)) -> rule2))]
("Gary" "is" "furry" "-")
((((triple5) -> (rule4 % int2))) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Fiona is not cold.
Unknown
inv-rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "cold" "-")
Harry is kind.
Unknown
rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "kind" "+")
Fiona is not furry.
Unknown
inv-rconc
[@2: Fiona is furry.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Fiona" "is" "furry" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
@0: Dave is blue.[(triple1)] Dave is nice.[(triple2)] Dave is white.[(triple3 OR ((((triple2) -> rule6)) -> rule1) OR ((((((triple1) -> rule4)) -> rule2)) -> rule5))] Fiona is kind.[(triple4)] Gary is blue.[(triple5)] Gary is nice.[(triple6)] Harry is cold.[(triple7)] @1: Dave is cold.[(((triple1) -> rule4))] Dave is kind.[(((triple2) -> rule6))] Fiona is white.[(((triple4) -> rule1))] Gary is cold.[(((triple5) -> rule4))] Gary is kind.[(((triple6) -> rule6))] Harry is furry.[(((triple7) -> rule2))] @2: Dave is furry.[(((((triple1) -> rule4)) -> rule2))] Gary is furry.[(((((triple5) -> rule4)) -> rule2))] Gary is white.[(((((triple6) -> rule6)) -> rule1) OR ((((((triple5) -> rule4)) -> rule2)) -> rule5))] Harry is white.[(((((triple7) -> rule2)) -> rule5))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple2
Dave is white.
("Dave" "is" "white" "+")
triple3
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
triple4
Gary is blue.
("Gary" "is" "blue" "+")
triple5
Gary is nice.
("Gary" "is" "nice" "+")
triple6
Harry is cold.
("Harry" "is" "cold" "+")
triple7
Dave is cold.
("Dave" "is" "cold" "+")
((triple1) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple2) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
((triple4) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((triple5) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple6) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple7) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
((((triple5) -> (rule4 % int2))) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((((triple6) -> (rule6 % int2))) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((((((triple5) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
((((triple7) -> (rule2 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2