Bob is blue. Bob is green. Bob is kind. Bob is round. Bob is smart. Bob is white. Bob is young. Erin is blue. Erin is green. Erin is not smart. Erin is not white. Erin is young. White people are smart. If Bob is kind then Bob is young. If Erin is young and Erin is not smart then Erin is round. Blue people are green. Round people are young. If someone is young and not kind then they are blue. All green, young people are blue. Round people are blue.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is not smart.
("Erin" "is" "smart" "-")
Erin is not white.
("Erin" "is" "white" "-")
Erin is young.
("Erin" "is" "young" "+")
White people are smart.
((("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
If Bob is kind then Bob is young.
((("Bob" "is" "kind" "+")) -> ("Bob" "is" "young" "+"))
If Erin is young and Erin is not smart then Erin is round.
((("Erin" "is" "young" "+") ("Erin" "is" "smart" "~")) -> ("Erin" "is" "round" "+"))
Blue people are green.
((("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
Round people are young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
If someone is young and not kind then they are blue.
((("someone" "is" "young" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "blue" "+"))
All green, young people are blue.
((("someone" "is" "green" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
Round people are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
Bob is green.
True
1
proof
[(triple2 OR ((triple1) -> rule4) OR ((((triple4) -> rule8)) -> rule4))]
("Bob" "is" "green" "+")
triple2
((triple1) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((((triple4) -> (rule8 % int2))) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Erin is not young.
False
1
inv-proof
[(triple12)]
("Erin" "is" "young" "-")
triple12
@0: Bob is blue.[(triple1 OR ((triple4) -> rule8) OR ((triple2 triple7) -> rule7) OR ((triple2 ((triple3) -> rule2)) -> rule7) OR ((triple2 ((triple4) -> rule5)) -> rule7))] Bob is green.[(triple2 OR ((triple1) -> rule4) OR ((((triple4) -> rule8)) -> rule4))] Bob is kind.[(triple3)] Bob is round.[(triple4)] Bob is smart.[(triple5 OR ((triple6) -> rule1))] Bob is white.[(triple6)] Bob is young.[(triple7 OR ((triple3) -> rule2) OR ((triple4) -> rule5))] Erin is blue.[(triple8 OR ((triple9 triple12) -> rule7) OR ((((triple12 triple10) -> rule3)) -> rule8))] Erin is green.[(triple9 OR ((triple8) -> rule4) OR ((((((triple12 triple10) -> rule3)) -> rule8)) -> rule4))] Erin is not smart.[(triple10)] Erin is not white.[(triple11)] Erin is young.[(triple12)] @1: Erin is round.[(((triple12 triple10) -> rule3))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
((triple4) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((triple2 triple7) -> (rule7 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((triple2 ((triple3) -> (rule2 % int2))) -> (rule7 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((triple2 ((triple4) -> (rule5 % int2))) -> (rule7 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
triple2
((triple1) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((((triple4) -> (rule8 % int2))) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
triple4
Bob is smart.
("Bob" "is" "smart" "+")
triple5
((triple6) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7
((triple3) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((triple4) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
triple8
((triple9 triple12) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((triple12 triple10) -> (rule3 % int2))) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
triple9
((triple8) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((((((triple12 triple10) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is not smart.
("Erin" "is" "smart" "-")
triple10
Erin is not white.
("Erin" "is" "white" "-")
triple11
Erin is young.
("Erin" "is" "young" "+")
triple12
Erin is round.
("Erin" "is" "round" "+")
((triple12 triple10) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1