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