Dave is blue. Dave is green. Dave is quiet. Dave is red. Dave is rough. Dave is round. Dave is smart. Fiona is blue. Fiona is green. Fiona is quiet. Fiona is round. Fiona is smart. If someone is green and quiet then they are red. If someone is rough and red then they are quiet. Green people are blue. All red people are rough. If someone is round and rough then they are red. All blue, smart people are red.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
If someone is green and quiet then they are red.
((("someone" "is" "green" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
If someone is rough and red then they are quiet.
((("someone" "is" "rough" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
Green people are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
All red people are rough.
((("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
If someone is round and rough then they are red.
((("someone" "is" "round" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
All blue, smart people are red.
((("someone" "is" "blue" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
Fiona is smart.
True
1
proof
[(triple12)]
("Fiona" "is" "smart" "+")
triple12
Dave is not smart.
False
1
inv-proof
[(triple7)]
("Dave" "is" "smart" "-")
triple7
Fiona is red.
True
3
proof
[(((triple8 triple12) -> rule6) OR ((triple9 triple10) -> rule1) OR ((((triple9) -> rule3) triple12) -> rule6))]
("Fiona" "is" "red" "+")
((triple8 triple12) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((triple9 triple10) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((((triple9) -> (rule3 % int2)) triple12) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is not red.
False
3
inv-proof
[(((triple8 triple12) -> rule6) OR ((triple9 triple10) -> rule1) OR ((((triple9) -> rule3) triple12) -> rule6))]
("Fiona" "is" "red" "-")
((triple8 triple12) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((triple9 triple10) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((((triple9) -> (rule3 % int2)) triple12) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is rough.
True
4
proof
[(((((triple8 triple12) -> rule6)) -> rule4) OR ((((triple9 triple10) -> rule1)) -> rule4) OR ((((((triple9) -> rule3) triple12) -> rule6)) -> rule4))]
("Fiona" "is" "rough" "+")
((((triple8 triple12) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
((((triple9 triple10) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
((((((triple9) -> (rule3 % int3)) triple12) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is not rough.
False
4
inv-proof
[(((((triple8 triple12) -> rule6)) -> rule4) OR ((((triple9 triple10) -> rule1)) -> rule4) OR ((((((triple9) -> rule3) triple12) -> rule6)) -> rule4))]
("Fiona" "is" "rough" "-")
((((triple8 triple12) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
((((triple9 triple10) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
((((((triple9) -> (rule3 % int3)) triple12) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
@0: Dave is blue.[(triple1 OR ((triple2) -> rule3))] Dave is green.[(triple2)] Dave is quiet.[(triple3 OR ((triple5 triple4) -> rule2) OR ((triple5 ((triple1 triple7) -> rule6)) -> rule2) OR ((triple5 ((triple6 triple5) -> rule5)) -> rule2) OR ((((triple4) -> rule4) triple4) -> rule2) OR ((((triple4) -> rule4) ((triple1 triple7) -> rule6)) -> rule2) OR ((((triple4) -> rule4) ((triple6 triple5) -> rule5)) -> rule2) OR ((triple5 ((((triple2) -> rule3) triple7) -> rule6)) -> rule2) OR ((((((triple1 triple7) -> rule6)) -> rule4) triple4) -> rule2) OR ((((triple4) -> rule4) ((((triple2) -> rule3) triple7) -> rule6)) -> rule2) OR ((((((triple1 triple7) -> rule6)) -> rule4) ((triple1 triple7) -> rule6)) -> rule2) OR ((((((triple1 triple7) -> rule6)) -> rule4) ((triple6 triple5) -> rule5)) -> rule2) OR ((((((triple1 triple7) -> rule6)) -> rule4) ((((triple2) -> rule3) triple7) -> rule6)) -> rule2) OR ((((((((triple2) -> rule3) triple7) -> rule6)) -> rule4) triple4) -> rule2) OR ((((((((triple2) -> rule3) triple7) -> rule6)) -> rule4) ((triple1 triple7) -> rule6)) -> rule2) OR ((((((((triple2) -> rule3) triple7) -> rule6)) -> rule4) ((triple6 triple5) -> rule5)) -> rule2) OR ((((((((triple2) -> rule3) triple7) -> rule6)) -> rule4) ((((triple2) -> rule3) triple7) -> rule6)) -> rule2))] Dave is red.[(triple4 OR ((triple1 triple7) -> rule6) OR ((triple2 triple3) -> rule1) OR ((triple6 triple5) -> rule5) OR ((((triple2) -> rule3) triple7) -> rule6))] Dave is rough.[(triple5 OR ((triple4) -> rule4) OR ((((triple1 triple7) -> rule6)) -> rule4) OR ((((triple2 triple3) -> rule1)) -> rule4) OR ((((((triple2) -> rule3) triple7) -> rule6)) -> rule4))] Dave is round.[(triple6)] Dave is smart.[(triple7)] Fiona is blue.[(triple8 OR ((triple9) -> rule3))] Fiona is green.[(triple9)] Fiona is quiet.[(triple10 OR ((((((triple8 triple12) -> rule6)) -> rule4) ((triple8 triple12) -> rule6)) -> rule2) OR ((((((triple8 triple12) -> rule6)) -> rule4) ((((triple9) -> rule3) triple12) -> rule6)) -> rule2) OR ((((((((triple9) -> rule3) triple12) -> rule6)) -> rule4) ((triple8 triple12) -> rule6)) -> rule2) OR ((((((((triple9) -> rule3) triple12) -> rule6)) -> rule4) ((((triple9) -> rule3) triple12) -> rule6)) -> rule2))] Fiona is round.[(triple11)] Fiona is smart.[(triple12)] @1: Fiona is red.[(((triple8 triple12) -> rule6) OR ((triple9 triple10) -> rule1) OR ((((triple9) -> rule3) triple12) -> rule6))] @2: Fiona is rough.[(((((triple8 triple12) -> rule6)) -> rule4) OR ((((triple9 triple10) -> rule1)) -> rule4) OR ((((((triple9) -> rule3) triple12) -> rule6)) -> rule4))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
((triple2) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
((triple5 triple4) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple5 ((triple1 triple7) -> (rule6 % int2))) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((triple5 ((triple6 triple5) -> (rule5 % int2))) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((triple4) -> (rule4 % int2)) triple4) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((((triple4) -> (rule4 % int3)) ((triple1 triple7) -> (rule6 % int2))) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((triple4) -> (rule4 % int3)) ((triple6 triple5) -> (rule5 % int2))) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((triple5 ((((triple2) -> (rule3 % int3)) triple7) -> (rule6 % int2))) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
((((((triple1 triple7) -> (rule6 % int3))) -> (rule4 % int2)) triple4) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
((((triple4) -> (rule4 % int4)) ((((triple2) -> (rule3 % int3)) triple7) -> (rule6 % int2))) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
((((((triple1 triple7) -> (rule6 % int3))) -> (rule4 % int2)) ((triple1 triple7) -> (rule6 % int3))) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
((((((triple1 triple7) -> (rule6 % int3))) -> (rule4 % int2)) ((triple6 triple5) -> (rule5 % int3))) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
((((((triple1 triple7) -> (rule6 % int4))) -> (rule4 % int3)) ((((triple2) -> (rule3 % int2)) triple7) -> (rule6 % int4))) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
((((((((triple2) -> (rule3 % int4)) triple7) -> (rule6 % int3))) -> (rule4 % int2)) triple4) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
((((((((triple2) -> (rule3 % int4)) triple7) -> (rule6 % int3))) -> (rule4 % int2)) ((triple1 triple7) -> (rule6 % int3))) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
((((((((triple2) -> (rule3 % int4)) triple7) -> (rule6 % int3))) -> (rule4 % int2)) ((triple6 triple5) -> (rule5 % int3))) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
((((((((triple2) -> (rule3 % int4)) triple7) -> (rule6 % int3))) -> (rule4 % int2)) ((((triple2) -> (rule3 % int4)) triple7) -> (rule6 % int3))) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is red.
("Dave" "is" "red" "+")
triple4
((triple1 triple7) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((triple2 triple3) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((triple6 triple5) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((((triple2) -> (rule3 % int2)) triple7) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
triple5
((triple4) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple1 triple7) -> (rule6 % int2))) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((triple2 triple3) -> (rule1 % int2))) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((((triple2) -> (rule3 % int3)) triple7) -> (rule6 % int2))) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
triple6
Dave is smart.
("Dave" "is" "smart" "+")
triple7
Fiona is blue.
("Fiona" "is" "blue" "+")
triple8
((triple9) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
triple9
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple10
((((((triple8 triple12) -> (rule6 % int3))) -> (rule4 % int2)) ((triple8 triple12) -> (rule6 % int3))) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
((((((triple8 triple12) -> (rule6 % int4))) -> (rule4 % int3)) ((((triple9) -> (rule3 % int2)) triple12) -> (rule6 % int4))) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
((((((((triple9) -> (rule3 % int4)) triple12) -> (rule6 % int3))) -> (rule4 % int2)) ((triple8 triple12) -> (rule6 % int3))) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
int4
((((((((triple9) -> (rule3 % int4)) triple12) -> (rule6 % int3))) -> (rule4 % int2)) ((((triple9) -> (rule3 % int4)) triple12) -> (rule6 % int3))) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
int4
Fiona is round.
("Fiona" "is" "round" "+")
triple11
Fiona is smart.
("Fiona" "is" "smart" "+")
triple12
Fiona is red.
("Fiona" "is" "red" "+")
((triple8 triple12) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((triple9 triple10) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((((triple9) -> (rule3 % int2)) triple12) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
((((triple8 triple12) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
((((triple9 triple10) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
((((((triple9) -> (rule3 % int3)) triple12) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3