Dave is cold. Dave is green. Dave is quiet. Red people are round. All green people are blue. If Dave is cold then Dave is red. Quiet people are smart. Smart, quiet people are round. Blue, quiet people are green. If someone is quiet then they are green. All green people are quiet.
Dave is cold.
("Dave" "is" "cold" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Red people are round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
All green people are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
If Dave is cold then Dave is red.
((("Dave" "is" "cold" "+")) -> ("Dave" "is" "red" "+"))
Quiet people are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
Smart, quiet people are round.
((("someone" "is" "smart" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
Blue, quiet people are green.
((("someone" "is" "blue" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
If someone is quiet then they are green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
All green people are quiet.
((("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
Dave is quiet.
True
1
proof
[(triple3 OR ((triple2) -> rule8))]
("Dave" "is" "quiet" "+")
triple3
((triple2) -> (rule8 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not green.
False
1
inv-proof
[(triple2 OR ((triple3) -> rule7))]
("Dave" "is" "green" "-")
triple2
((triple3) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
True
2
proof
[(((triple1) -> rule3))]
("Dave" "is" "red" "+")
((triple1) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is not blue.
False
2
inv-proof
[(((triple2) -> rule2) OR ((((triple3) -> rule7)) -> rule2))]
("Dave" "is" "blue" "-")
((triple2) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple3) -> (rule7 % int2))) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is round.
True
3
proof
[(((((triple1) -> rule3)) -> rule1) OR ((((triple3) -> rule4) triple3) -> rule5) OR ((((triple3) -> rule4) ((triple2) -> rule8)) -> rule5) OR ((((((triple2) -> rule8)) -> rule4) triple3) -> rule5) OR ((((((triple2) -> rule8)) -> rule4) ((triple2) -> rule8)) -> rule5))]
("Dave" "is" "round" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((triple3) -> (rule4 % int2)) triple3) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple3) -> (rule4 % int3)) ((triple2) -> (rule8 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
((((((triple2) -> (rule8 % int3))) -> (rule4 % int2)) triple3) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
((((((triple2) -> (rule8 % int3))) -> (rule4 % int2)) ((triple2) -> (rule8 % int3))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is not round.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1) OR ((((triple3) -> rule4) triple3) -> rule5) OR ((((triple3) -> rule4) ((triple2) -> rule8)) -> rule5) OR ((((((triple2) -> rule8)) -> rule4) triple3) -> rule5) OR ((((((triple2) -> rule8)) -> rule4) ((triple2) -> rule8)) -> rule5))]
("Dave" "is" "round" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((triple3) -> (rule4 % int2)) triple3) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple3) -> (rule4 % int3)) ((triple2) -> (rule8 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
((((((triple2) -> (rule8 % int3))) -> (rule4 % int2)) triple3) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
((((((triple2) -> (rule8 % int3))) -> (rule4 % int2)) ((triple2) -> (rule8 % int3))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
@0: Dave is cold.[(triple1)] Dave is green.[(triple2 OR ((triple3) -> rule7))] Dave is quiet.[(triple3 OR ((triple2) -> rule8))] @1: Dave is blue.[(((triple2) -> rule2) OR ((((triple3) -> rule7)) -> rule2))] Dave is red.[(((triple1) -> rule3))] Dave is smart.[(((triple3) -> rule4) OR ((((triple2) -> rule8)) -> rule4))] @2: Dave is round.[(((((triple1) -> rule3)) -> rule1) OR ((((triple3) -> rule4) triple3) -> rule5) OR ((((triple3) -> rule4) ((triple2) -> rule8)) -> rule5) OR ((((((triple2) -> rule8)) -> rule4) triple3) -> rule5) OR ((((((triple2) -> rule8)) -> rule4) ((triple2) -> rule8)) -> rule5))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
((triple3) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
((triple2) -> (rule8 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((triple2) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple3) -> (rule7 % int2))) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((triple1) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple3) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((((triple2) -> (rule8 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((triple3) -> (rule4 % int2)) triple3) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple3) -> (rule4 % int3)) ((triple2) -> (rule8 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
((((((triple2) -> (rule8 % int3))) -> (rule4 % int2)) triple3) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
((((((triple2) -> (rule8 % int3))) -> (rule4 % int2)) ((triple2) -> (rule8 % int3))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3