Bob is kind. Bob is quiet. Bob is round. Bob is not smart. Bob is white. Bob is young. Dave is kind. Dave is smart. Dave is white. Dave is young. If Bob is young and Bob is white then Bob is round. All round people are white. If someone is blue and not young then they are not white. Young people are white. Kind, young people are quiet. If someone is quiet then they are not blue. If someone is young and quiet then they are round. Quiet, round people are kind.
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is not smart.
("Bob" "is" "smart" "-")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
If Bob is young and Bob is white then Bob is round.
((("Bob" "is" "young" "+") ("Bob" "is" "white" "+")) -> ("Bob" "is" "round" "+"))
All round people are white.
((("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
If someone is blue and not young then they are not white.
((("someone" "is" "blue" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "white" "-"))
Young people are white.
((("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
Kind, young people are quiet.
((("someone" "is" "kind" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
If someone is quiet then they are not blue.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "-"))
If someone is young and quiet then they are round.
((("someone" "is" "young" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
Quiet, round people are kind.
((("someone" "is" "quiet" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
Dave is white.
True
1
proof
[(triple9 OR ((triple10) -> rule4) OR ((((triple10 ((triple7 triple10) -> rule5)) -> rule7)) -> rule2))]
("Dave" "is" "white" "+")
triple9
((triple10) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((((triple10 ((triple7 triple10) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Bob is not white.
False
1
inv-proof
[(triple5 OR ((triple3) -> rule2) OR ((triple6) -> rule4) OR ((((triple6 triple2) -> rule7)) -> rule2) OR ((((triple6 ((triple1 triple6) -> rule5)) -> rule7)) -> rule2))]
("Bob" "is" "white" "-")
triple5
((triple3) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple6) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((((triple6 triple2) -> (rule7 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((triple6 ((triple1 triple6) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Dave is quiet.
True
3
proof
[(((triple7 triple10) -> rule5))]
("Dave" "is" "quiet" "+")
((triple7 triple10) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Bob is blue.
False
2
inv-proof
[(((triple2) -> rule6) OR ((((triple1 triple6) -> rule5)) -> rule6))]
("Bob" "is" "blue" "+")
((triple2) -> (rule6 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
((((triple1 triple6) -> (rule5 % int2))) -> (rule6 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
@0: Bob is kind.[(triple1 OR ((triple2 triple3) -> rule8) OR ((triple2 ((triple6 triple2) -> rule7)) -> rule8) OR ((triple2 ((triple6 triple5) -> rule1)) -> rule8) OR ((triple2 ((triple6 ((triple6) -> rule4)) -> rule1)) -> rule8))] Bob is not smart.[(triple4)] Bob is quiet.[(triple2 OR ((triple1 triple6) -> rule5))] Bob is round.[(triple3 OR ((triple6 triple2) -> rule7) OR ((triple6 triple5) -> rule1) OR ((triple6 ((triple6) -> rule4)) -> rule1) OR ((triple6 ((triple1 triple6) -> rule5)) -> rule7))] Bob is white.[(triple5 OR ((triple3) -> rule2) OR ((triple6) -> rule4) OR ((((triple6 triple2) -> rule7)) -> rule2) OR ((((triple6 ((triple1 triple6) -> rule5)) -> rule7)) -> rule2))] Bob is young.[(triple6)] Dave is kind.[(triple7)] Dave is smart.[(triple8)] Dave is white.[(triple9 OR ((triple10) -> rule4) OR ((((triple10 ((triple7 triple10) -> rule5)) -> rule7)) -> rule2))] Dave is young.[(triple10)] @1: Bob is not blue.[(((triple2) -> rule6) OR ((((triple1 triple6) -> rule5)) -> rule6))] Dave is quiet.[(((triple7 triple10) -> rule5))] @2: Dave is not blue.[(((((triple7 triple10) -> rule5)) -> rule6))] Dave is round.[(((triple10 ((triple7 triple10) -> rule5)) -> rule7))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
((triple2 triple3) -> (rule8 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple2 ((triple6 triple2) -> (rule7 % int2))) -> (rule8 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((triple2 ((triple6 triple5) -> (rule1 % int2))) -> (rule8 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((triple2 ((triple6 ((triple6) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is not smart.
("Bob" "is" "smart" "-")
triple4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
((triple1 triple6) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple3
((triple6 triple2) -> (rule7 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple6 triple5) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple6 ((triple6) -> (rule4 % int2))) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((triple6 ((triple1 triple6) -> (rule5 % int2))) -> (rule7 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
triple5
((triple3) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple6) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((((triple6 triple2) -> (rule7 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((triple6 ((triple1 triple6) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
triple6
Dave is kind.
("Dave" "is" "kind" "+")
triple7
Dave is smart.
("Dave" "is" "smart" "+")
triple8
Dave is white.
("Dave" "is" "white" "+")
triple9
((triple10) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((((triple10 ((triple7 triple10) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
triple10
Bob is not blue.
("Bob" "is" "blue" "-")
((triple2) -> (rule6 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
((((triple1 triple6) -> (rule5 % int2))) -> (rule6 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple7 triple10) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not blue.
("Dave" "is" "blue" "-")
((((triple7 triple10) -> (rule5 % int2))) -> (rule6 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
((triple10 ((triple7 triple10) -> (rule5 % int2))) -> (rule7 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2