Bob is blue. Charlie is not cold. Fiona is red. Harry is nice. Blue things are nice. All nice things are not red. If something is cold and not red then it is green. If something is green then it is not kind. All young, blue things are kind. Green things are young.
Bob is blue.
("Bob" "is" "blue" "+")
Charlie is not cold.
("Charlie" "is" "cold" "-")
Fiona is red.
("Fiona" "is" "red" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Blue things are nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
All nice things are not red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "-"))
If something is cold and not red then it is green.
((("something" "is" "cold" "+") ("something" "is" "red" "~")) -> ("something" "is" "green" "+"))
If something is green then it is not kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "-"))
All young, blue things are kind.
((("something" "is" "young" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
Green things are young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
Bob is blue.
True
1
proof
[(triple1)]
("Bob" "is" "blue" "+")
triple1
Bob is not blue.
False
1
inv-proof
[(triple1)]
("Bob" "is" "blue" "-")
triple1
Bob is nice.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "nice" "+")
((triple1) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is not nice.
False
2
inv-proof
[(((triple1) -> rule1))]
("Bob" "is" "nice" "-")
((triple1) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is not red.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("Bob" "is" "red" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is red.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("Bob" "is" "red" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Charlie is not young.
Unknown
inv-rconc
[@2: Charlie is young.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Charlie" "is" "young" "-")
Charlie is nice.
Unknown
rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "nice" "+")
Fiona is not young.
Unknown
inv-rconc
[@2: Fiona is young.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Fiona" "is" "young" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
@0: Bob is blue.[(triple1)] Charlie is not cold.[(triple2)] Fiona is red.[(triple3)] Harry is nice.[(triple4)] @1: Bob is nice.[(((triple1) -> rule1))] Harry is not red.[(((triple4) -> rule2))] @2: Bob is not red.[(((((triple1) -> rule1)) -> rule2))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple2
Fiona is red.
("Fiona" "is" "red" "+")
triple3
Harry is nice.
("Harry" "is" "nice" "+")
triple4
Bob is nice.
("Bob" "is" "nice" "+")
((triple1) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Harry is not red.
("Harry" "is" "red" "-")
((triple4) -> (rule2 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Bob is not red.
("Bob" "is" "red" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2