Charlie is blue. Charlie is furry. Charlie is green. Charlie is quiet. Charlie is red. Charlie is white. Charlie is young. Fiona is blue. Fiona is furry. Fiona is green. Fiona is quiet. Fiona is red. Fiona is white. Fiona is young. If someone is young and green then they are quiet. If someone is red then they are blue.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Fiona is young.
("Fiona" "is" "young" "+")
If someone is young and green then they are quiet.
((("someone" "is" "young" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
If someone is red then they are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
Charlie is blue.
True
1
proof
[(triple1 OR ((triple5) -> rule2))]
("Charlie" "is" "blue" "+")
triple1
((triple5) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is not white.
False
1
inv-proof
[(triple6)]
("Charlie" "is" "white" "-")
triple6
@0: Charlie is blue.[(triple1 OR ((triple5) -> rule2))] Charlie is furry.[(triple2)] Charlie is green.[(triple3)] Charlie is quiet.[(triple4 OR ((triple7 triple3) -> rule1))] Charlie is red.[(triple5)] Charlie is white.[(triple6)] Charlie is young.[(triple7)] Fiona is blue.[(triple8 OR ((triple12) -> rule2))] Fiona is furry.[(triple9)] Fiona is green.[(triple10)] Fiona is quiet.[(triple11 OR ((triple14 triple10) -> rule1))] Fiona is red.[(triple12)] Fiona is white.[(triple13)] Fiona is young.[(triple14)]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
((triple5) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
((triple7 triple3) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple5
Charlie is white.
("Charlie" "is" "white" "+")
triple6
Charlie is young.
("Charlie" "is" "young" "+")
triple7
Fiona is blue.
("Fiona" "is" "blue" "+")
triple8
((triple12) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
triple9
Fiona is green.
("Fiona" "is" "green" "+")
triple10
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple11
((triple14 triple10) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
triple12
Fiona is white.
("Fiona" "is" "white" "+")
triple13
Fiona is young.
("Fiona" "is" "young" "+")
triple14