Charlie is blue. Charlie is not green. Charlie is kind. Charlie is nice. Charlie is quiet. Charlie is smart. Charlie is white. Erin is blue. Erin is green. Erin is kind. Erin is nice. Erin is quiet. Erin is smart. Erin is white. If someone is kind and nice then they are smart. If someone is blue and not green then they are white. All quiet, white people are kind.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is not green.
("Charlie" "is" "green" "-")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
If someone is kind and nice then they are smart.
((("someone" "is" "kind" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
If someone is blue and not green then they are white.
((("someone" "is" "blue" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "white" "+"))
All quiet, white people are kind.
((("someone" "is" "quiet" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
Charlie is kind.
True
1
proof
[(triple3 OR ((triple5 triple7) -> rule3) OR ((triple5 ((triple1 triple2) -> rule2)) -> rule3))]
("Charlie" "is" "kind" "+")
triple3
((triple5 triple7) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple5 ((triple1 triple2) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Erin is not smart.
False
1
inv-proof
[(triple13 OR ((triple10 triple11) -> rule1) OR ((((triple12 triple14) -> rule3) triple11) -> rule1))]
("Erin" "is" "smart" "-")
triple13
((triple10 triple11) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple12 triple14) -> (rule3 % int2)) triple11) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
@0: Charlie is blue.[(triple1)] Charlie is kind.[(triple3 OR ((triple5 triple7) -> rule3) OR ((triple5 ((triple1 triple2) -> rule2)) -> rule3))] Charlie is nice.[(triple4)] Charlie is not green.[(triple2)] Charlie is quiet.[(triple5)] Charlie is smart.[(triple6 OR ((triple3 triple4) -> rule1) OR ((((triple5 triple7) -> rule3) triple4) -> rule1) OR ((((triple5 ((triple1 triple2) -> rule2)) -> rule3) triple4) -> rule1))] Charlie is white.[(triple7 OR ((triple1 triple2) -> rule2))] Erin is blue.[(triple8)] Erin is green.[(triple9)] Erin is kind.[(triple10 OR ((triple12 triple14) -> rule3))] Erin is nice.[(triple11)] Erin is quiet.[(triple12)] Erin is smart.[(triple13 OR ((triple10 triple11) -> rule1) OR ((((triple12 triple14) -> rule3) triple11) -> rule1))] Erin is white.[(triple14)]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
((triple5 triple7) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple5 ((triple1 triple2) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Charlie is not green.
("Charlie" "is" "green" "-")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple5
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
((triple3 triple4) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((((triple5 triple7) -> (rule3 % int2)) triple4) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple5 ((triple1 triple2) -> (rule2 % int3))) -> (rule3 % int2)) triple4) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
triple7
((triple1 triple2) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
triple8
Erin is green.
("Erin" "is" "green" "+")
triple9
Erin is kind.
("Erin" "is" "kind" "+")
triple10
((triple12 triple14) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
triple11
Erin is quiet.
("Erin" "is" "quiet" "+")
triple12
Erin is smart.
("Erin" "is" "smart" "+")
triple13
((triple10 triple11) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple12 triple14) -> (rule3 % int2)) triple11) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
triple14