Bob is big. Bob is blue. Bob is cold. Bob is kind. Bob is quiet. Charlie is blue. Charlie is cold. Charlie is green. Charlie is young. Dave is green. Dave is kind. Gary is blue. Gary is cold. Gary is green. Gary is kind. Gary is young. Young people are cold. If Charlie is young and Charlie is blue then Charlie is big. If Dave is young and Dave is big then Dave is blue. Big people are quiet. Cold people are quiet. All blue people are green.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is young.
("Gary" "is" "young" "+")
Young people are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
If Charlie is young and Charlie is blue then Charlie is big.
((("Charlie" "is" "young" "+") ("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "big" "+"))
If Dave is young and Dave is big then Dave is blue.
((("Dave" "is" "young" "+") ("Dave" "is" "big" "+")) -> ("Dave" "is" "blue" "+"))
Big people are quiet.
((("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
Cold people are quiet.
((("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
All blue people are green.
((("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
Charlie is green.
True
1
proof
[(triple8 OR ((triple6) -> rule6))]
("Charlie" "is" "green" "+")
triple8
((triple6) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is not blue.
False
1
inv-proof
[(triple6)]
("Charlie" "is" "blue" "-")
triple6
Dave is not blue.
Unknown
inv-rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "blue" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Bob is big.[(triple1)] Bob is blue.[(triple2)] Bob is cold.[(triple3)] Bob is kind.[(triple4)] Bob is quiet.[(triple5 OR ((triple1) -> rule4) OR ((triple3) -> rule5))] Charlie is blue.[(triple6)] Charlie is cold.[(triple7 OR ((triple9) -> rule1))] Charlie is green.[(triple8 OR ((triple6) -> rule6))] Charlie is young.[(triple9)] Dave is green.[(triple10)] Dave is kind.[(triple11)] Gary is blue.[(triple12)] Gary is cold.[(triple13 OR ((triple16) -> rule1))] Gary is green.[(triple14 OR ((triple12) -> rule6))] Gary is kind.[(triple15)] Gary is young.[(triple16)] @1: Bob is green.[(((triple2) -> rule6))] Charlie is big.[(((triple9 triple6) -> rule2))] Charlie is quiet.[(((triple7) -> rule5) OR ((((triple9) -> rule1)) -> rule5) OR ((((triple9 triple6) -> rule2)) -> rule4))] Gary is quiet.[(((triple13) -> rule5) OR ((((triple16) -> rule1)) -> rule5))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is cold.
("Bob" "is" "cold" "+")
triple3
Bob is kind.
("Bob" "is" "kind" "+")
triple4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
((triple1) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple3) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple6
Charlie is cold.
("Charlie" "is" "cold" "+")
triple7
((triple9) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
triple8
((triple6) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
triple9
Dave is green.
("Dave" "is" "green" "+")
triple10
Dave is kind.
("Dave" "is" "kind" "+")
triple11
Gary is blue.
("Gary" "is" "blue" "+")
triple12
Gary is cold.
("Gary" "is" "cold" "+")
triple13
((triple16) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
triple14
((triple12) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple15
Gary is young.
("Gary" "is" "young" "+")
triple16
Bob is green.
("Bob" "is" "green" "+")
((triple2) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((triple9 triple6) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple7) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((((triple9) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((triple9 triple6) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple13) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((triple16) -> (rule1 % int2))) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2