Charlie is cold. Charlie is green. Charlie is nice. Charlie is round. Charlie is smart. Charlie is young. Dave is cold. Dave is green. Dave is nice. Dave is round. Dave is smart. Dave is young. All quiet things are green. All quiet things are green. All nice things are young. If something is smart then it is young. Cold things are quiet. If something is smart and quiet then it is round. If something is quiet then it is cold. If Charlie is round and Charlie is not quiet then Charlie is green.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
All quiet things are green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
All quiet things are green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
All nice things are young.
((("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
If something is smart then it is young.
((("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
Cold things are quiet.
((("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
If something is smart and quiet then it is round.
((("something" "is" "smart" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
If something is quiet then it is cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
If Charlie is round and Charlie is not quiet then Charlie is green.
((("Charlie" "is" "round" "+") ("Charlie" "is" "quiet" "~")) -> ("Charlie" "is" "green" "+"))
Charlie is cold.
True
1
proof
[(triple1)]
("Charlie" "is" "cold" "+")
triple1
Dave is not smart.
False
1
inv-proof
[(triple11)]
("Dave" "is" "smart" "-")
triple11
Dave is quiet.
True
2
proof
[(((triple7) -> rule5))]
("Dave" "is" "quiet" "+")
((triple7) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not quiet.
False
2
inv-proof
[(((triple7) -> rule5))]
("Dave" "is" "quiet" "-")
((triple7) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
@0: Charlie is cold.[(triple1)] Charlie is green.[(triple2 OR ((((triple1) -> rule5)) -> rule1) OR ((((triple1) -> rule5)) -> rule2))] Charlie is nice.[(triple3)] Charlie is round.[(triple4 OR ((triple5 ((triple1) -> rule5)) -> rule6))] Charlie is smart.[(triple5)] Charlie is young.[(triple6 OR ((triple3) -> rule3) OR ((triple5) -> rule4))] Dave is cold.[(triple7)] Dave is green.[(triple8 OR ((((triple7) -> rule5)) -> rule1) OR ((((triple7) -> rule5)) -> rule2))] Dave is nice.[(triple9)] Dave is round.[(triple10 OR ((triple11 ((triple7) -> rule5)) -> rule6))] Dave is smart.[(triple11)] Dave is young.[(triple12 OR ((triple11) -> rule4) OR ((triple9) -> rule3))] @1: Charlie is quiet.[(((triple1) -> rule5))] Dave is quiet.[(((triple7) -> rule5))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is round.
("Charlie" "is" "round" "+")
triple4
((triple5 ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
Charlie is young.
("Charlie" "is" "young" "+")
triple6
((triple3) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple5) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
triple7
Dave is green.
("Dave" "is" "green" "+")
triple8
((((triple7) -> (rule5 % int2))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((((triple7) -> (rule5 % int2))) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
triple9
Dave is round.
("Dave" "is" "round" "+")
triple10
((triple11 ((triple7) -> (rule5 % int2))) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
triple11
Dave is young.
("Dave" "is" "young" "+")
triple12
((triple11) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple9) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple1) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple7) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1