Bob is cold. Bob is green. Bob is not kind. Bob is quiet. Bob is red. Bob is smart. Bob is young. Gary is cold. Gary is green. Gary is smart. If something is kind then it is green. All young things are red. If something is cold and not green then it is red. If something is green and not red then it is quiet. If something is young and not red then it is smart. All red things are smart.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is not kind.
("Bob" "is" "kind" "-")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If something is kind then it is green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
All young things are red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
If something is cold and not green then it is red.
((("something" "is" "cold" "+") ("something" "is" "green" "~")) -> ("something" "is" "red" "+"))
If something is green and not red then it is quiet.
((("something" "is" "green" "+") ("something" "is" "red" "~")) -> ("something" "is" "quiet" "+"))
If something is young and not red then it is smart.
((("something" "is" "young" "+") ("something" "is" "red" "~")) -> ("something" "is" "smart" "+"))
All red things are smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
Bob is cold.
True
1
proof
[(triple1)]
("Bob" "is" "cold" "+")
triple1
Bob is not quiet.
False
1
inv-proof
[(triple4)]
("Bob" "is" "quiet" "-")
triple4
Gary is not quiet.
Unknown
inv-rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "quiet" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
@0: Bob is cold.[(triple1)] Bob is green.[(triple2)] Bob is not kind.[(triple3)] Bob is quiet.[(triple4)] Bob is red.[(triple5 OR ((triple7) -> rule2))] Bob is smart.[(triple6 OR ((triple5) -> rule6) OR ((((triple7) -> rule2)) -> rule6))] Bob is young.[(triple7)] Gary is cold.[(triple8)] Gary is green.[(triple9)] Gary is smart.[(triple10)]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is not kind.
("Bob" "is" "kind" "-")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is red.
("Bob" "is" "red" "+")
triple5
((triple7) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
triple6
((triple5) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
triple7
Gary is cold.
("Gary" "is" "cold" "+")
triple8
Gary is green.
("Gary" "is" "green" "+")
triple9
Gary is smart.
("Gary" "is" "smart" "+")
triple10