Bob is cold. Bob is kind. Bob is young. Charlie is furry. Charlie is kind. Charlie is young. Dave is cold. Dave is young. Gary is blue. Gary is furry. Gary is kind. Gary is young. If Gary is young then Gary is kind. All young people are blue. If someone is smart then they are furry.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is young.
("Gary" "is" "young" "+")
If Gary is young then Gary is kind.
((("Gary" "is" "young" "+")) -> ("Gary" "is" "kind" "+"))
All young people are blue.
((("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
If someone is smart then they are furry.
((("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
Charlie is young.
True
1
proof
[(triple6)]
("Charlie" "is" "young" "+")
triple6
Charlie is not furry.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "furry" "-")
triple4
Charlie is blue.
True
2
proof
[(((triple6) -> rule2))]
("Charlie" "is" "blue" "+")
((triple6) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is not blue.
False
2
inv-proof
[(((triple6) -> rule2))]
("Charlie" "is" "blue" "-")
((triple6) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Bob is not furry.
Unknown
inv-rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "furry" "-")
Dave is furry.
Unknown
rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "furry" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Bob is cold.[(triple1)] Bob is kind.[(triple2)] Bob is young.[(triple3)] Charlie is furry.[(triple4)] Charlie is kind.[(triple5)] Charlie is young.[(triple6)] Dave is cold.[(triple7)] Dave is young.[(triple8)] Gary is blue.[(triple9 OR ((triple12) -> rule2))] Gary is furry.[(triple10)] Gary is kind.[(triple11 OR ((triple12) -> rule1))] Gary is young.[(triple12)] @1: Bob is blue.[(((triple3) -> rule2))] Charlie is blue.[(((triple6) -> rule2))] Dave is blue.[(((triple8) -> rule2))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
Charlie is furry.
("Charlie" "is" "furry" "+")
triple4
Charlie is kind.
("Charlie" "is" "kind" "+")
triple5
Charlie is young.
("Charlie" "is" "young" "+")
triple6
Dave is cold.
("Dave" "is" "cold" "+")
triple7
Dave is young.
("Dave" "is" "young" "+")
triple8
Gary is blue.
("Gary" "is" "blue" "+")
triple9
((triple12) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
triple10
Gary is kind.
("Gary" "is" "kind" "+")
triple11
((triple12) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
triple12
Bob is blue.
("Bob" "is" "blue" "+")
((triple3) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple6) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((triple8) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1