Dave is cold. Dave is green. Dave is quiet. Dave is red. Dave is round. Dave is smart. Dave is young. Fiona is cold. Fiona is green. Fiona is quiet. Fiona is red. Fiona is round. Fiona is smart. Fiona is young. If something is round then it is cold. Young, green things are cold. All smart things are young.
Dave is cold.
("Dave" "is" "cold" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is green.
("Fiona" "is" "green" "+")
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 young.
("Fiona" "is" "young" "+")
If something is round then it is cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
Young, green things are cold.
((("something" "is" "young" "+") ("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
All smart things are young.
((("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
Dave is young.
True
1
proof
[(triple7 OR ((triple6) -> rule3))]
("Dave" "is" "young" "+")
triple7
((triple6) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Fiona is not red.
False
1
inv-proof
[(triple11)]
("Fiona" "is" "red" "-")
triple11
@0: Dave is cold.[(triple1 OR ((triple5) -> rule1) OR ((triple7 triple2) -> rule2) OR ((((triple6) -> rule3) triple2) -> rule2))] Dave is green.[(triple2)] Dave is quiet.[(triple3)] Dave is red.[(triple4)] Dave is round.[(triple5)] Dave is smart.[(triple6)] Dave is young.[(triple7 OR ((triple6) -> rule3))] Fiona is cold.[(triple8 OR ((triple12) -> rule1) OR ((triple14 triple9) -> rule2) OR ((((triple13) -> rule3) triple9) -> rule2))] Fiona is green.[(triple9)] Fiona is quiet.[(triple10)] Fiona is red.[(triple11)] Fiona is round.[(triple12)] Fiona is smart.[(triple13)] Fiona is young.[(triple14 OR ((triple13) -> rule3))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
((triple5) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((triple7 triple2) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((triple6) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Dave is red.
("Dave" "is" "red" "+")
triple4
Dave is round.
("Dave" "is" "round" "+")
triple5
Dave is smart.
("Dave" "is" "smart" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
((triple6) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple8
((triple12) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple14 triple9) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((((triple13) -> (rule3 % int2)) triple9) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
triple9
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple10
Fiona is red.
("Fiona" "is" "red" "+")
triple11
Fiona is round.
("Fiona" "is" "round" "+")
triple12
Fiona is smart.
("Fiona" "is" "smart" "+")
triple13
Fiona is young.
("Fiona" "is" "young" "+")
triple14
((triple13) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1