Bob is green. Charlie is green. Gary is nice. If someone is green then they are red. If someone is young then they are quiet. If someone is round then they are green. All red people are green. Blue people are red. All green people are quiet.
Bob is green.
("Bob" "is" "green" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
If someone is green then they are red.
((("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
If someone is young then they are quiet.
((("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
If someone is round then they are green.
((("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
All red people are green.
((("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
Blue people are red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
All green people are quiet.
((("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
Bob is green.
True
1
proof
[(triple1)]
("Bob" "is" "green" "+")
triple1
Charlie is not green.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "green" "-")
triple2
Charlie is red.
True
2
proof
[(((triple2) -> rule1))]
("Charlie" "is" "red" "+")
((triple2) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Bob is not quiet.
False
2
inv-proof
[(((triple1) -> rule6))]
("Bob" "is" "quiet" "-")
((triple1) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Gary is not red.
Unknown
inv-rconc
[@3: Gary is red.[CWA. Example of deepest failure = (rule1 <- rule4 <- rule5 <- FAIL)]]
("Gary" "is" "red" "-")
Gary is quiet.
Unknown
rconc
[@4: Gary is quiet.[CWA. Example of deepest failure = (rule6 <- rule4 <- rule1 <- rule3 <- FAIL)]]
("Gary" "is" "quiet" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Bob is green.[(triple1)] Charlie is green.[(triple2)] Gary is nice.[(triple3)] @1: Bob is quiet.[(((triple1) -> rule6))] Bob is red.[(((triple1) -> rule1))] Charlie is quiet.[(((triple2) -> rule6))] Charlie is red.[(((triple2) -> rule1))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Gary is nice.
("Gary" "is" "nice" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple1) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((triple1) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple2) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((triple2) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1