Fiona is big. Fiona is blue. Fiona is cold. Fiona is kind. Fiona is nice. Fiona is round. Fiona is smart. Harry is big. Harry is blue. Harry is cold. Harry is round. Harry is smart. If Harry is round and Harry is kind then Harry is big. If Harry is big and Harry is nice then Harry is kind. All smart, cold things are big. All big, smart things are kind. All smart things are nice. All big, nice things are kind. If Harry is kind then Harry is big. If something is smart then it is kind.
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Harry is round and Harry is kind then Harry is big.
((("Harry" "is" "round" "+") ("Harry" "is" "kind" "+")) -> ("Harry" "is" "big" "+"))
If Harry is big and Harry is nice then Harry is kind.
((("Harry" "is" "big" "+") ("Harry" "is" "nice" "+")) -> ("Harry" "is" "kind" "+"))
All smart, cold things are big.
((("something" "is" "smart" "+") ("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
All big, smart things are kind.
((("something" "is" "big" "+") ("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
All smart things are nice.
((("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
All big, nice things are kind.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
If Harry is kind then Harry is big.
((("Harry" "is" "kind" "+")) -> ("Harry" "is" "big" "+"))
If something is smart then it is kind.
((("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
Fiona is cold.
True
1
proof
[(triple3)]
("Fiona" "is" "cold" "+")
triple3
Fiona is not round.
False
1
inv-proof
[(triple6)]
("Fiona" "is" "round" "-")
triple6
Harry is kind.
True
2
proof
[(((triple12) -> rule8) OR ((triple8 triple12) -> rule4) OR ((triple8 ((triple12) -> rule5)) -> rule2) OR ((triple8 ((triple12) -> rule5)) -> rule6) OR ((((triple12 triple10) -> rule3) triple12) -> rule4) OR ((((triple12 triple10) -> rule3) ((triple12) -> rule5)) -> rule2) OR ((((triple12 triple10) -> rule3) ((triple12) -> rule5)) -> rule6))]
("Harry" "is" "kind" "+")
((triple12) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple8 triple12) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple8 ((triple12) -> (rule5 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((triple8 ((triple12) -> (rule5 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple12 triple10) -> (rule3 % int2)) triple12) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
((((triple12 triple10) -> (rule3 % int3)) ((triple12) -> (rule5 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
((((triple12 triple10) -> (rule3 % int3)) ((triple12) -> (rule5 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is not kind.
False
2
inv-proof
[(((triple12) -> rule8) OR ((triple8 triple12) -> rule4) OR ((triple8 ((triple12) -> rule5)) -> rule2) OR ((triple8 ((triple12) -> rule5)) -> rule6) OR ((((triple12 triple10) -> rule3) triple12) -> rule4) OR ((((triple12 triple10) -> rule3) ((triple12) -> rule5)) -> rule2) OR ((((triple12 triple10) -> rule3) ((triple12) -> rule5)) -> rule6))]
("Harry" "is" "kind" "-")
((triple12) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple8 triple12) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple8 ((triple12) -> (rule5 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((triple8 ((triple12) -> (rule5 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple12 triple10) -> (rule3 % int2)) triple12) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
((((triple12 triple10) -> (rule3 % int3)) ((triple12) -> (rule5 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
((((triple12 triple10) -> (rule3 % int3)) ((triple12) -> (rule5 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
@0: Fiona is big.[(triple1 OR ((triple7 triple3) -> rule3))] Fiona is blue.[(triple2)] Fiona is cold.[(triple3)] Fiona is kind.[(triple4 OR ((triple7) -> rule8) OR ((triple1 triple5) -> rule6) OR ((triple1 triple7) -> rule4) OR ((triple1 ((triple7) -> rule5)) -> rule6) OR ((((triple7 triple3) -> rule3) triple5) -> rule6) OR ((((triple7 triple3) -> rule3) triple7) -> rule4) OR ((((triple7 triple3) -> rule3) ((triple7) -> rule5)) -> rule6))] Fiona is nice.[(triple5 OR ((triple7) -> rule5))] Fiona is round.[(triple6)] Fiona is smart.[(triple7)] Harry is big.[(triple8 OR ((triple12 triple10) -> rule3) OR ((((triple12) -> rule8)) -> rule7) OR ((triple11 ((triple12) -> rule8)) -> rule1))] Harry is blue.[(triple9)] Harry is cold.[(triple10)] Harry is round.[(triple11)] Harry is smart.[(triple12)] @1: Harry is kind.[(((triple12) -> rule8) OR ((triple8 triple12) -> rule4) OR ((triple8 ((triple12) -> rule5)) -> rule2) OR ((triple8 ((triple12) -> rule5)) -> rule6) OR ((((triple12 triple10) -> rule3) triple12) -> rule4) OR ((((triple12 triple10) -> rule3) ((triple12) -> rule5)) -> rule2) OR ((((triple12 triple10) -> rule3) ((triple12) -> rule5)) -> rule6))] Harry is nice.[(((triple12) -> rule5))]
Fiona is big.
("Fiona" "is" "big" "+")
triple1
((triple7 triple3) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
triple2
Fiona is cold.
("Fiona" "is" "cold" "+")
triple3
Fiona is kind.
("Fiona" "is" "kind" "+")
triple4
((triple7) -> (rule8 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
((triple1 triple5) -> (rule6 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
((triple1 triple7) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
((triple1 ((triple7) -> (rule5 % int2))) -> (rule6 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
((((triple7 triple3) -> (rule3 % int2)) triple5) -> (rule6 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
((((triple7 triple3) -> (rule3 % int2)) triple7) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
((((triple7 triple3) -> (rule3 % int3)) ((triple7) -> (rule5 % int2))) -> (rule6 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
triple5
((triple7) -> (rule5 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
triple6
Fiona is smart.
("Fiona" "is" "smart" "+")
triple7
Harry is big.
("Harry" "is" "big" "+")
triple8
((triple12 triple10) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((((triple12) -> (rule8 % int2))) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((triple11 ((triple12) -> (rule8 % int2))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
triple9
Harry is cold.
("Harry" "is" "cold" "+")
triple10
Harry is round.
("Harry" "is" "round" "+")
triple11
Harry is smart.
("Harry" "is" "smart" "+")
triple12
Harry is kind.
("Harry" "is" "kind" "+")
((triple12) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple8 triple12) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple8 ((triple12) -> (rule5 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((triple8 ((triple12) -> (rule5 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple12 triple10) -> (rule3 % int2)) triple12) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
((((triple12 triple10) -> (rule3 % int3)) ((triple12) -> (rule5 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
((((triple12 triple10) -> (rule3 % int3)) ((triple12) -> (rule5 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
((triple12) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1