Charlie is blue. Charlie is cold. Charlie is quiet. Charlie is red. Charlie is not smart. Charlie is white. Charlie is young. Erin is blue. Erin is cold. Erin is not quiet. Erin is red. Erin is smart. Erin is white. Erin is young. If something is smart and not quiet then it is white. All cold things are young.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is not smart.
("Charlie" "is" "smart" "-")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is not quiet.
("Erin" "is" "quiet" "-")
Erin is red.
("Erin" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
If something is smart and not quiet then it is white.
((("something" "is" "smart" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "white" "+"))
All cold things are young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
Erin is blue.
True
1
proof
[(triple8)]
("Erin" "is" "blue" "+")
triple8
Charlie is not red.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "red" "-")
triple4
@0: Charlie is blue.[(triple1)] Charlie is cold.[(triple2)] Charlie is not smart.[(triple5)] Charlie is quiet.[(triple3)] Charlie is red.[(triple4)] Charlie is white.[(triple6)] Charlie is young.[(triple7 OR ((triple2) -> rule2))] Erin is blue.[(triple8)] Erin is cold.[(triple9)] Erin is not quiet.[(triple10)] Erin is red.[(triple11)] Erin is smart.[(triple12)] Erin is white.[(triple13 OR ((triple12 triple10) -> rule1))] Erin is young.[(triple14 OR ((triple9) -> rule2))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is not smart.
("Charlie" "is" "smart" "-")
triple5
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Charlie is white.
("Charlie" "is" "white" "+")
triple6
Charlie is young.
("Charlie" "is" "young" "+")
triple7
((triple2) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
triple8
Erin is cold.
("Erin" "is" "cold" "+")
triple9
Erin is not quiet.
("Erin" "is" "quiet" "-")
triple10
Erin is red.
("Erin" "is" "red" "+")
triple11
Erin is smart.
("Erin" "is" "smart" "+")
triple12
Erin is white.
("Erin" "is" "white" "+")
triple13
((triple12 triple10) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
triple14
((triple9) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1