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