Fiona is big. Fiona is cold. Fiona is green. Fiona is quiet. Fiona is rough. Harry is big. Harry is cold. Harry is green. Harry is nice. Harry is quiet. Harry is rough. Harry is smart. Cold people are smart. If someone is quiet and nice then they are smart. If someone is cold then they are quiet. If Harry is rough and Harry is nice then Harry is smart. If someone is green then they are nice. If someone is quiet then they are big.
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Cold people are smart.
((("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
If someone is quiet and nice then they are smart.
((("someone" "is" "quiet" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
If someone is cold then they are quiet.
((("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
If Harry is rough and Harry is nice then Harry is smart.
((("Harry" "is" "rough" "+") ("Harry" "is" "nice" "+")) -> ("Harry" "is" "smart" "+"))
If someone is green then they are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
If someone is quiet then they are big.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
Harry is cold.
True
1
proof
[(triple7)]
("Harry" "is" "cold" "+")
triple7
Fiona is not quiet.
False
1
inv-proof
[(triple4 OR ((triple2) -> rule3))]
("Fiona" "is" "quiet" "-")
triple4
((triple2) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
@0: Fiona is big.[(triple1 OR ((triple4) -> rule6) OR ((((triple2) -> rule3)) -> rule6))] Fiona is cold.[(triple2)] Fiona is green.[(triple3)] Fiona is quiet.[(triple4 OR ((triple2) -> rule3))] Fiona is rough.[(triple5)] Harry is big.[(triple6 OR ((triple10) -> rule6) OR ((((triple7) -> rule3)) -> rule6))] Harry is cold.[(triple7)] Harry is green.[(triple8)] Harry is nice.[(triple9 OR ((triple8) -> rule5))] Harry is quiet.[(triple10 OR ((triple7) -> rule3))] Harry is rough.[(triple11)] Harry is smart.[(triple12 OR ((triple7) -> rule1) OR ((triple10 triple9) -> rule2) OR ((triple11 triple9) -> rule4) OR ((triple10 ((triple8) -> rule5)) -> rule2) OR ((triple11 ((triple8) -> rule5)) -> rule4) OR ((((triple7) -> rule3) triple9) -> rule2) OR ((((triple7) -> rule3) ((triple8) -> rule5)) -> rule2))] @1: Fiona is nice.[(((triple3) -> rule5))] Fiona is smart.[(((triple2) -> rule1) OR ((triple4 ((triple3) -> rule5)) -> rule2) OR ((((triple2) -> rule3) ((triple3) -> rule5)) -> rule2))]
Fiona is big.
("Fiona" "is" "big" "+")
triple1
((triple4) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
triple2
Fiona is green.
("Fiona" "is" "green" "+")
triple3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple4
((triple2) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
triple5
Harry is big.
("Harry" "is" "big" "+")
triple6
((triple10) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((((triple7) -> (rule3 % int2))) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
triple7
Harry is green.
("Harry" "is" "green" "+")
triple8
Harry is nice.
("Harry" "is" "nice" "+")
triple9
((triple8) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
((triple7) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
triple11
Harry is smart.
("Harry" "is" "smart" "+")
triple12
((triple7) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((triple10 triple9) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((triple11 triple9) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((triple10 ((triple8) -> (rule5 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((triple11 ((triple8) -> (rule5 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple7) -> (rule3 % int2)) triple9) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple7) -> (rule3 % int3)) ((triple8) -> (rule5 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple3) -> (rule5 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple4 ((triple3) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
((((triple2) -> (rule3 % int3)) ((triple3) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3