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