Charlie is big. Charlie is furry. Charlie is green. Charlie is nice. Charlie is quiet. Fiona is big. Fiona is furry. Fiona is green. Fiona is kind. Fiona is nice. Fiona is quiet. Fiona is red. Quiet things are red. If something is furry then it is quiet.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Quiet things are red.
((("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
If something is furry then it is quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
Fiona is furry.
True
1
proof
[(triple7)]
("Fiona" "is" "furry" "+")
triple7
Charlie is not furry.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "furry" "-")
triple2
Charlie is red.
True
2
proof
[(((triple5) -> rule1) OR ((((triple2) -> rule2)) -> rule1))]
("Charlie" "is" "red" "+")
((triple5) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not red.
False
2
inv-proof
[(((triple5) -> rule1) OR ((((triple2) -> rule2)) -> rule1))]
("Charlie" "is" "red" "-")
((triple5) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
@0: Charlie is big.[(triple1)] Charlie is furry.[(triple2)] Charlie is green.[(triple3)] Charlie is nice.[(triple4)] Charlie is quiet.[(triple5 OR ((triple2) -> rule2))] Fiona is big.[(triple6)] Fiona is furry.[(triple7)] Fiona is green.[(triple8)] Fiona is kind.[(triple9)] Fiona is nice.[(triple10)] Fiona is quiet.[(triple11 OR ((triple7) -> rule2))] Fiona is red.[(triple12 OR ((triple11) -> rule1) OR ((((triple7) -> rule2)) -> rule1))] @1: Charlie is red.[(((triple5) -> rule1) OR ((((triple2) -> rule2)) -> rule1))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple5
((triple2) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
triple6
Fiona is furry.
("Fiona" "is" "furry" "+")
triple7
Fiona is green.
("Fiona" "is" "green" "+")
triple8
Fiona is kind.
("Fiona" "is" "kind" "+")
triple9
Fiona is nice.
("Fiona" "is" "nice" "+")
triple10
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple11
((triple7) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
triple12
((triple11) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
((triple5) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2