Bob is blue. Bob is not green. Bob is nice. Bob is quiet. Bob is red. Bob is round. Fiona is not green. Fiona is not nice. Fiona is quiet. Fiona is not round. Harry is furry. Harry is not green. Harry is nice. Harry is red. Harry is round. Blue things are furry. All red things are blue. All quiet things are red. If Fiona is green and Fiona is not red then Fiona is furry. If Fiona is nice then Fiona is round. If Bob is red and Bob is not blue then Bob is green. Quiet, nice things are round. If something is green then it is nice.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is not green.
("Bob" "is" "green" "-")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Fiona is not green.
("Fiona" "is" "green" "-")
Fiona is not nice.
("Fiona" "is" "nice" "-")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is not round.
("Fiona" "is" "round" "-")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is not green.
("Harry" "is" "green" "-")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
Blue things are furry.
((("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
All red things are blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
All quiet things are red.
((("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
If Fiona is green and Fiona is not red then Fiona is furry.
((("Fiona" "is" "green" "+") ("Fiona" "is" "red" "~")) -> ("Fiona" "is" "furry" "+"))
If Fiona is nice then Fiona is round.
((("Fiona" "is" "nice" "+")) -> ("Fiona" "is" "round" "+"))
If Bob is red and Bob is not blue then Bob is green.
((("Bob" "is" "red" "+") ("Bob" "is" "blue" "~")) -> ("Bob" "is" "green" "+"))
Quiet, nice things are round.
((("something" "is" "quiet" "+") ("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
If something is green then it is nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
Bob is red.
True
1
proof
[(triple5 OR ((triple4) -> rule3))]
("Bob" "is" "red" "+")
triple5
((triple4) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Harry is green.
False
1
inv-proof
[(triple12)]
("Harry" "is" "green" "+")
triple12
Bob is furry.
True
2
proof
[(((triple1) -> rule1) OR ((((triple5) -> rule2)) -> rule1) OR ((((((triple4) -> rule3)) -> rule2)) -> rule1))]
("Bob" "is" "furry" "+")
((triple1) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Harry is not blue.
False
2
inv-proof
[(((triple14) -> rule2))]
("Harry" "is" "blue" "-")
((triple14) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Fiona is blue.
True
3
proof
[(((((triple9) -> rule3)) -> rule2))]
("Fiona" "is" "blue" "+")
((((triple9) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is not blue.
False
3
inv-proof
[(((((triple9) -> rule3)) -> rule2))]
("Fiona" "is" "blue" "-")
((((triple9) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is furry.
True
4
proof
[(((((((triple9) -> rule3)) -> rule2)) -> rule1))]
("Fiona" "is" "furry" "+")
((((((triple9) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is not furry.
False
4
inv-proof
[(((((((triple9) -> rule3)) -> rule2)) -> rule1))]
("Fiona" "is" "furry" "-")
((((((triple9) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
@0: Bob is blue.[(triple1 OR ((triple5) -> rule2) OR ((((triple4) -> rule3)) -> rule2))] Bob is nice.[(triple3)] Bob is not green.[(triple2)] Bob is quiet.[(triple4)] Bob is red.[(triple5 OR ((triple4) -> rule3))] Bob is round.[(triple6 OR ((triple4 triple3) -> rule7))] Fiona is not green.[(triple7)] Fiona is not nice.[(triple8)] Fiona is not round.[(triple10)] Fiona is quiet.[(triple9)] Harry is furry.[(triple11 OR ((((triple14) -> rule2)) -> rule1))] Harry is nice.[(triple13)] Harry is not green.[(triple12)] Harry is red.[(triple14)] Harry is round.[(triple15)] @1: Bob is furry.[(((triple1) -> rule1) OR ((((triple5) -> rule2)) -> rule1) OR ((((((triple4) -> rule3)) -> rule2)) -> rule1))] Fiona is red.[(((triple9) -> rule3))] Harry is blue.[(((triple14) -> rule2))] @2: Fiona is blue.[(((((triple9) -> rule3)) -> rule2))] @3: Fiona is furry.[(((((((triple9) -> rule3)) -> rule2)) -> rule1))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
((triple5) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is not green.
("Bob" "is" "green" "-")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is red.
("Bob" "is" "red" "+")
triple5
((triple4) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple6
((triple4 triple3) -> (rule7 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Fiona is not green.
("Fiona" "is" "green" "-")
triple7
Fiona is not nice.
("Fiona" "is" "nice" "-")
triple8
Fiona is not round.
("Fiona" "is" "round" "-")
triple10
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple9
Harry is furry.
("Harry" "is" "furry" "+")
triple11
((((triple14) -> (rule2 % int2))) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
triple13
Harry is not green.
("Harry" "is" "green" "-")
triple12
Harry is red.
("Harry" "is" "red" "+")
triple14
Harry is round.
("Harry" "is" "round" "+")
triple15
Bob is furry.
("Bob" "is" "furry" "+")
((triple1) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
((triple9) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple14) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
((((triple9) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
((((((triple9) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3