Bob is kind. Erin is nice. Erin is white. Fiona is big. Fiona is green. Harry is cold. Harry is furry. All kind, white things are cold. If something is nice then it is kind.
Bob is kind.
("Bob" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
All kind, white things are cold.
((("something" "is" "kind" "+") ("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
If something is nice then it is kind.
((("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
Bob is kind.
True
1
proof
[(triple1)]
("Bob" "is" "kind" "+")
triple1
Harry is not furry.
False
1
inv-proof
[(triple7)]
("Harry" "is" "furry" "-")
triple7
Erin is kind.
True
2
proof
[(((triple2) -> rule2))]
("Erin" "is" "kind" "+")
((triple2) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is not kind.
False
2
inv-proof
[(((triple2) -> rule2))]
("Erin" "is" "kind" "-")
((triple2) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is cold.
True
4
proof
[(((((triple2) -> rule2) triple3) -> rule1))]
("Erin" "is" "cold" "+")
((((triple2) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is not cold.
False
4
inv-proof
[(((((triple2) -> rule2) triple3) -> rule1))]
("Erin" "is" "cold" "-")
((((triple2) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Harry is not kind.
Unknown
inv-rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "kind" "-")
Bob is cold.
Unknown
rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "cold" "+")
Fiona is not kind.
Unknown
inv-rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "kind" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Bob is kind.[(triple1)] Erin is nice.[(triple2)] Erin is white.[(triple3)] Fiona is big.[(triple4)] Fiona is green.[(triple5)] Harry is cold.[(triple6)] Harry is furry.[(triple7)] @1: Erin is kind.[(((triple2) -> rule2))] @2: Erin is cold.[(((((triple2) -> rule2) triple3) -> rule1))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Erin is nice.
("Erin" "is" "nice" "+")
triple2
Erin is white.
("Erin" "is" "white" "+")
triple3
Fiona is big.
("Fiona" "is" "big" "+")
triple4
Fiona is green.
("Fiona" "is" "green" "+")
triple5
Harry is cold.
("Harry" "is" "cold" "+")
triple6
Harry is furry.
("Harry" "is" "furry" "+")
triple7
Erin is kind.
("Erin" "is" "kind" "+")
((triple2) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((((triple2) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2