Bob is not big. Bob is blue. Bob is quiet. Bob is red. Bob is round. Fiona is big. Fiona is blue. Fiona is nice. Fiona is quiet. Fiona is red. Fiona is rough. Fiona is round. If something is quiet then it is rough. All rough things are nice. Big things are quiet. If something is big and not red then it is blue. If Fiona is round and Fiona is not quiet then Fiona is not nice. If Bob is blue and Bob is not quiet then Bob is nice.
Bob is not big.
("Bob" "is" "big" "-")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Fiona is big.
("Fiona" "is" "big" "+")
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 rough.
("Fiona" "is" "rough" "+")
Fiona is round.
("Fiona" "is" "round" "+")
If something is quiet then it is rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
All rough things are nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
Big things are quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
If something is big and not red then it is blue.
((("something" "is" "big" "+") ("something" "is" "red" "~")) -> ("something" "is" "blue" "+"))
If Fiona is round and Fiona is not quiet then Fiona is not nice.
((("Fiona" "is" "round" "+") ("Fiona" "is" "quiet" "~")) -> ("Fiona" "is" "nice" "-"))
If Bob is blue and Bob is not quiet then Bob is nice.
((("Bob" "is" "blue" "+") ("Bob" "is" "quiet" "~")) -> ("Bob" "is" "nice" "+"))
Fiona is nice.
True
1
proof
[(triple8 OR ((triple11) -> rule2) OR ((((triple9) -> rule1)) -> rule2) OR ((((((triple6) -> rule3)) -> rule1)) -> rule2))]
("Fiona" "is" "nice" "+")
triple8
((triple11) -> (rule2 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
((((((triple6) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Bob is big.
False
1
inv-proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
Bob is rough.
True
2
proof
[(((triple3) -> rule1))]
("Bob" "is" "rough" "+")
((triple3) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is not rough.
False
2
inv-proof
[(((triple3) -> rule1))]
("Bob" "is" "rough" "-")
((triple3) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
True
3
proof
[(((((triple3) -> rule1)) -> rule2))]
("Bob" "is" "nice" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is not nice.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule2))]
("Bob" "is" "nice" "-")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
@0: Bob is blue.[(triple2)] Bob is not big.[(triple1)] Bob is quiet.[(triple3)] Bob is red.[(triple4)] Bob is round.[(triple5)] Fiona is big.[(triple6)] Fiona is blue.[(triple7)] Fiona is nice.[(triple8 OR ((triple11) -> rule2) OR ((((triple9) -> rule1)) -> rule2) OR ((((((triple6) -> rule3)) -> rule1)) -> rule2))] Fiona is quiet.[(triple9 OR ((triple6) -> rule3))] Fiona is red.[(triple10)] Fiona is rough.[(triple11 OR ((triple9) -> rule1) OR ((((triple6) -> rule3)) -> rule1))] Fiona is round.[(triple12)] @1: Bob is rough.[(((triple3) -> rule1))] @2: Bob is nice.[(((((triple3) -> rule1)) -> rule2))]
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is not big.
("Bob" "is" "big" "-")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
triple5
Fiona is big.
("Fiona" "is" "big" "+")
triple6
Fiona is blue.
("Fiona" "is" "blue" "+")
triple7
Fiona is nice.
("Fiona" "is" "nice" "+")
triple8
((triple11) -> (rule2 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
((((((triple6) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple9
((triple6) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
triple10
Fiona is rough.
("Fiona" "is" "rough" "+")
triple11
((triple9) -> (rule1 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
((((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
triple12
Bob is rough.
("Bob" "is" "rough" "+")
((triple3) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2