Bob is not cold. Dave is red. Fiona is kind. Fiona is white. Fiona is young. Harry is green. Harry is young. If Dave is cold and Dave is kind then Dave is red. All white, green people are nice. Green people are white. All young, white people are cold. All cold, red people are green. Green, kind people are young.
Bob is not cold.
("Bob" "is" "cold" "-")
Dave is red.
("Dave" "is" "red" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is young.
("Harry" "is" "young" "+")
If Dave is cold and Dave is kind then Dave is red.
((("Dave" "is" "cold" "+") ("Dave" "is" "kind" "+")) -> ("Dave" "is" "red" "+"))
All white, green people are nice.
((("someone" "is" "white" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
Green people are white.
((("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
All young, white people are cold.
((("someone" "is" "young" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
All cold, red people are green.
((("someone" "is" "cold" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
Green, kind people are young.
((("someone" "is" "green" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
Harry is young.
True
1
proof
[(triple7)]
("Harry" "is" "young" "+")
triple7
Bob is cold.
False
1
inv-proof
[(triple1)]
("Bob" "is" "cold" "+")
triple1
Harry is white.
True
2
proof
[(((triple6) -> rule3))]
("Harry" "is" "white" "+")
((triple6) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Fiona is not cold.
False
3
inv-proof
[(((triple5 triple4) -> rule4))]
("Fiona" "is" "cold" "-")
((triple5 triple4) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Harry is nice.
True
4
proof
[(((((triple6) -> rule3) triple6) -> rule2))]
("Harry" "is" "nice" "+")
((((triple6) -> (rule3 % int2)) triple6) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not cold.
False
4
inv-proof
[(((triple7 ((triple6) -> rule3)) -> rule4))]
("Harry" "is" "cold" "-")
((triple7 ((triple6) -> (rule3 % int2))) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Dave is not cold.
Unknown
inv-rconc
[@2: Dave is cold.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("Dave" "is" "cold" "-")
Bob is nice.
Unknown
rconc
[@2: Bob is nice.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Bob" "is" "nice" "+")
Fiona is not nice.
Unknown
inv-rconc
[@2: Fiona is nice.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Fiona" "is" "nice" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Bob is not cold.[(triple1)] Dave is red.[(triple2)] Fiona is kind.[(triple3)] Fiona is white.[(triple4)] Fiona is young.[(triple5)] Harry is green.[(triple6)] Harry is young.[(triple7)] @1: Fiona is cold.[(((triple5 triple4) -> rule4))] Harry is white.[(((triple6) -> rule3))] @2: Harry is cold.[(((triple7 ((triple6) -> rule3)) -> rule4))] Harry is nice.[(((((triple6) -> rule3) triple6) -> rule2))]
Bob is not cold.
("Bob" "is" "cold" "-")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Fiona is kind.
("Fiona" "is" "kind" "+")
triple3
Fiona is white.
("Fiona" "is" "white" "+")
triple4
Fiona is young.
("Fiona" "is" "young" "+")
triple5
Harry is green.
("Harry" "is" "green" "+")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple5 triple4) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple6) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple7 ((triple6) -> (rule3 % int2))) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((((triple6) -> (rule3 % int2)) triple6) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2