Fiona is cold. Fiona is green. Fiona is kind. Fiona is quiet. Fiona is rough. Fiona is round. Fiona is smart. Harry is cold. Harry is green. Harry is kind. Harry is quiet. Harry is rough. Harry is round. Harry is smart. If something is round and smart then it is kind. All round, rough things are kind. Smart, quiet things are rough. Cold things are kind. Green things are kind. If something is rough then it is smart.
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If something is round and smart then it is kind.
((("something" "is" "round" "+") ("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
All round, rough things are kind.
((("something" "is" "round" "+") ("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
Smart, quiet things are rough.
((("something" "is" "smart" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
Cold things are kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
Green things are kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
If something is rough then it is smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
Harry is kind.
True
1
proof
[(triple10 OR ((triple8) -> rule4) OR ((triple9) -> rule5) OR ((triple13 triple12) -> rule2) OR ((triple13 triple14) -> rule1) OR ((triple13 ((triple12) -> rule6)) -> rule1) OR ((triple13 ((triple14 triple11) -> rule3)) -> rule2))]
("Harry" "is" "kind" "+")
triple10
((triple8) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple9) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple13 triple12) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple13 triple14) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple13 ((triple12) -> (rule6 % int2))) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((triple13 ((triple14 triple11) -> (rule3 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not kind.
False
1
inv-proof
[(triple10 OR ((triple8) -> rule4) OR ((triple9) -> rule5) OR ((triple13 triple12) -> rule2) OR ((triple13 triple14) -> rule1) OR ((triple13 ((triple12) -> rule6)) -> rule1) OR ((triple13 ((triple14 triple11) -> rule3)) -> rule2))]
("Harry" "is" "kind" "-")
triple10
((triple8) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple9) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple13 triple12) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple13 triple14) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple13 ((triple12) -> (rule6 % int2))) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((triple13 ((triple14 triple11) -> (rule3 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
@0: Fiona is cold.[(triple1)] Fiona is green.[(triple2)] Fiona is kind.[(triple3 OR ((triple1) -> rule4) OR ((triple2) -> rule5) OR ((triple6 triple5) -> rule2) OR ((triple6 triple7) -> rule1) OR ((triple6 ((triple5) -> rule6)) -> rule1) OR ((triple6 ((triple7 triple4) -> rule3)) -> rule2))] Fiona is quiet.[(triple4)] Fiona is rough.[(triple5 OR ((triple7 triple4) -> rule3))] Fiona is round.[(triple6)] Fiona is smart.[(triple7 OR ((triple5) -> rule6))] Harry is cold.[(triple8)] Harry is green.[(triple9)] Harry is kind.[(triple10 OR ((triple8) -> rule4) OR ((triple9) -> rule5) OR ((triple13 triple12) -> rule2) OR ((triple13 triple14) -> rule1) OR ((triple13 ((triple12) -> rule6)) -> rule1) OR ((triple13 ((triple14 triple11) -> rule3)) -> rule2))] Harry is quiet.[(triple11)] Harry is rough.[(triple12 OR ((triple14 triple11) -> rule3))] Harry is round.[(triple13)] Harry is smart.[(triple14 OR ((triple12) -> rule6))]
Fiona is cold.
("Fiona" "is" "cold" "+")
triple1
Fiona is green.
("Fiona" "is" "green" "+")
triple2
Fiona is kind.
("Fiona" "is" "kind" "+")
triple3
((triple1) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
((triple2) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
((triple6 triple5) -> (rule2 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
((triple6 triple7) -> (rule1 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
((triple6 ((triple5) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((triple6 ((triple7 triple4) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple4
Fiona is rough.
("Fiona" "is" "rough" "+")
triple5
((triple7 triple4) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
triple6
Fiona is smart.
("Fiona" "is" "smart" "+")
triple7
((triple5) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
triple8
Harry is green.
("Harry" "is" "green" "+")
triple9
Harry is kind.
("Harry" "is" "kind" "+")
triple10
((triple8) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple9) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple13 triple12) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple13 triple14) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple13 ((triple12) -> (rule6 % int2))) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((triple13 ((triple14 triple11) -> (rule3 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
Harry is rough.
("Harry" "is" "rough" "+")
triple12
((triple14 triple11) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple13
Harry is smart.
("Harry" "is" "smart" "+")
triple14
((triple12) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1