Bob is big. Bob is blue. Bob is cold. Bob is furry. Bob is kind. Bob is quiet. Bob is white. Fiona is big. Fiona is blue. Fiona is cold. Fiona is furry. Fiona is quiet. If someone is white then they are quiet. If someone is cold then they are kind. If someone is kind then they are white.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is white.
("Bob" "is" "white" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
If someone is white then they are quiet.
((("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
If someone is cold then they are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
If someone is kind then they are white.
((("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
Fiona is blue.
True
1
proof
[(triple9)]
("Fiona" "is" "blue" "+")
triple9
Bob is not furry.
False
1
inv-proof
[(triple4)]
("Bob" "is" "furry" "-")
triple4
Fiona is kind.
True
2
proof
[(((triple10) -> rule2))]
("Fiona" "is" "kind" "+")
((triple10) -> (rule2 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is not kind.
False
2
inv-proof
[(((triple10) -> rule2))]
("Fiona" "is" "kind" "-")
((triple10) -> (rule2 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
@0: Bob is big.[(triple1)] Bob is blue.[(triple2)] Bob is cold.[(triple3)] Bob is furry.[(triple4)] Bob is kind.[(triple5 OR ((triple3) -> rule2))] Bob is quiet.[(triple6 OR ((triple7) -> rule1) OR ((((triple5) -> rule3)) -> rule1) OR ((((((triple3) -> rule2)) -> rule3)) -> rule1))] Bob is white.[(triple7 OR ((triple5) -> rule3) OR ((((triple3) -> rule2)) -> rule3))] Fiona is big.[(triple8)] Fiona is blue.[(triple9)] Fiona is cold.[(triple10)] Fiona is furry.[(triple11)] Fiona is quiet.[(triple12 OR ((((((triple10) -> rule2)) -> rule3)) -> rule1))] @1: Fiona is kind.[(((triple10) -> rule2))] @2: Fiona is white.[(((((triple10) -> rule2)) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is cold.
("Bob" "is" "cold" "+")
triple3
Bob is furry.
("Bob" "is" "furry" "+")
triple4
Bob is kind.
("Bob" "is" "kind" "+")
triple5
((triple3) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple6
((triple7) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
triple7
((triple5) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
triple8
Fiona is blue.
("Fiona" "is" "blue" "+")
triple9
Fiona is cold.
("Fiona" "is" "cold" "+")
triple10
Fiona is furry.
("Fiona" "is" "furry" "+")
triple11
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple12
((((((triple10) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple10) -> (rule2 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
((((triple10) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2