Bob is blue. Bob is green. Bob is quiet. Bob is young. Fiona is blue. Fiona is nice. Fiona is quiet. Fiona is red. Fiona is white. Fiona is young. All nice things are white. Nice, white things are red. All blue things are nice.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is young.
("Bob" "is" "young" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Fiona is young.
("Fiona" "is" "young" "+")
All nice things are white.
((("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
Nice, white things are red.
((("something" "is" "nice" "+") ("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
All blue things are nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
Fiona is white.
True
1
proof
[(triple9 OR ((triple6) -> rule1) OR ((((triple5) -> rule3)) -> rule1))]
("Fiona" "is" "white" "+")
triple9
((triple6) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is not blue.
False
1
inv-proof
[(triple5)]
("Fiona" "is" "blue" "-")
triple5
Bob is nice.
True
2
proof
[(((triple1) -> rule3))]
("Bob" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is not nice.
False
2
inv-proof
[(((triple1) -> rule3))]
("Bob" "is" "nice" "-")
((triple1) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is white.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("Bob" "is" "white" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is not white.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("Bob" "is" "white" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is red.
True
6
proof
[(((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule1)) -> rule2))]
("Bob" "is" "red" "+")
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is not red.
False
6
inv-proof
[(((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule1)) -> rule2))]
("Bob" "is" "red" "-")
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
@0: Bob is blue.[(triple1)] Bob is green.[(triple2)] Bob is quiet.[(triple3)] Bob is young.[(triple4)] Fiona is blue.[(triple5)] Fiona is nice.[(triple6 OR ((triple5) -> rule3))] Fiona is quiet.[(triple7)] Fiona is red.[(triple8 OR ((triple6 triple9) -> rule2) OR ((triple6 ((triple6) -> rule1)) -> rule2) OR ((((triple5) -> rule3) triple9) -> rule2) OR ((((triple5) -> rule3) ((triple6) -> rule1)) -> rule2) OR ((triple6 ((((triple5) -> rule3)) -> rule1)) -> rule2) OR ((((triple5) -> rule3) ((((triple5) -> rule3)) -> rule1)) -> rule2))] Fiona is white.[(triple9 OR ((triple6) -> rule1) OR ((((triple5) -> rule3)) -> rule1))] Fiona is young.[(triple10)] @1: Bob is nice.[(((triple1) -> rule3))] @2: Bob is white.[(((((triple1) -> rule3)) -> rule1))] @3: Bob is red.[(((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule1)) -> rule2))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Bob is young.
("Bob" "is" "young" "+")
triple4
Fiona is blue.
("Fiona" "is" "blue" "+")
triple5
Fiona is nice.
("Fiona" "is" "nice" "+")
triple6
((triple5) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple7
Fiona is red.
("Fiona" "is" "red" "+")
triple8
((triple6 triple9) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((triple6 ((triple6) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
((((triple5) -> (rule3 % int2)) triple9) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
((((triple5) -> (rule3 % int3)) ((triple6) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
((triple6 ((((triple5) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
((((triple5) -> (rule3 % int3)) ((((triple5) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
triple9
((triple6) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
triple10
Bob is nice.
("Bob" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3