Bob is not big. Bob is blue. Bob is cold. Bob is not kind. Bob is red. Bob is not rough. Fiona is blue. Fiona is red. Fiona is rough. Fiona is white. If something is kind then it is red. If something is rough then it is kind. Big things are not cold. Kind, big things are white. Rough, white things are big. If something is cold and not kind then it is blue.
Bob is not big.
("Bob" "is" "big" "-")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is not kind.
("Bob" "is" "kind" "-")
Bob is red.
("Bob" "is" "red" "+")
Bob is not rough.
("Bob" "is" "rough" "-")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is white.
("Fiona" "is" "white" "+")
If something is kind then it is red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
If something is rough then it is kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
Big things are not cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "-"))
Kind, big things are white.
((("something" "is" "kind" "+") ("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
Rough, white things are big.
((("something" "is" "rough" "+") ("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
If something is cold and not kind then it is blue.
((("something" "is" "cold" "+") ("something" "is" "kind" "~")) -> ("something" "is" "blue" "+"))
Bob is not rough.
True
1
proof
[(triple6)]
("Bob" "is" "rough" "-")
triple6
Bob is rough.
False
1
inv-proof
[(triple6)]
("Bob" "is" "rough" "+")
triple6
Fiona is big.
True
3
proof
[(((triple9 triple10) -> rule5))]
("Fiona" "is" "big" "+")
((triple9 triple10) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is not big.
False
3
inv-proof
[(((triple9 triple10) -> rule5))]
("Fiona" "is" "big" "-")
((triple9 triple10) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is not cold.
True
4
proof
[(((((triple9 triple10) -> rule5)) -> rule3))]
("Fiona" "is" "cold" "-")
((((triple9 triple10) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is not cold.
("Fiona" "is" "cold" "-")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is cold.
False
4
inv-proof
[(((((triple9 triple10) -> rule5)) -> rule3))]
("Fiona" "is" "cold" "+")
((((triple9 triple10) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is not cold.
("Fiona" "is" "cold" "-")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
@0: Bob is blue.[(triple2 OR ((triple3 triple4) -> rule6))] Bob is cold.[(triple3)] Bob is not big.[(triple1)] Bob is not kind.[(triple4)] Bob is not rough.[(triple6)] Bob is red.[(triple5)] Fiona is blue.[(triple7)] Fiona is red.[(triple8 OR ((((triple9) -> rule2)) -> rule1))] Fiona is rough.[(triple9)] Fiona is white.[(triple10)] @1: Fiona is big.[(((triple9 triple10) -> rule5))] Fiona is kind.[(((triple9) -> rule2))] @2: Fiona is not cold.[(((((triple9 triple10) -> rule5)) -> rule3))]
Bob is blue.
("Bob" "is" "blue" "+")
triple2
((triple3 triple4) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
triple3
Bob is not big.
("Bob" "is" "big" "-")
triple1
Bob is not kind.
("Bob" "is" "kind" "-")
triple4
Bob is not rough.
("Bob" "is" "rough" "-")
triple6
Bob is red.
("Bob" "is" "red" "+")
triple5
Fiona is blue.
("Fiona" "is" "blue" "+")
triple7
Fiona is red.
("Fiona" "is" "red" "+")
triple8
((((triple9) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
triple9
Fiona is white.
("Fiona" "is" "white" "+")
triple10
Fiona is big.
("Fiona" "is" "big" "+")
((triple9 triple10) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple9) -> (rule2 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is not cold.
("Fiona" "is" "cold" "-")
((((triple9 triple10) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is not cold.
("Fiona" "is" "cold" "-")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2