Dave is blue. Dave is cold. Dave is kind. Dave is quiet. Dave is smart. Dave is white. Dave is not young. Fiona is blue. Fiona is cold. Fiona is kind. Fiona is quiet. Fiona is smart. Fiona is white. Fiona is young. If someone is quiet and not blue then they are white. All quiet people are white. If someone is kind and not quiet then they are cold. Quiet, young people are cold. If Fiona is blue then Fiona is kind. If Fiona is cold then Fiona is smart.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is not young.
("Dave" "is" "young" "-")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Fiona is young.
("Fiona" "is" "young" "+")
If someone is quiet and not blue then they are white.
((("someone" "is" "quiet" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "white" "+"))
All quiet people are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
If someone is kind and not quiet then they are cold.
((("someone" "is" "kind" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "cold" "+"))
Quiet, young people are cold.
((("someone" "is" "quiet" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
If Fiona is blue then Fiona is kind.
((("Fiona" "is" "blue" "+")) -> ("Fiona" "is" "kind" "+"))
If Fiona is cold then Fiona is smart.
((("Fiona" "is" "cold" "+")) -> ("Fiona" "is" "smart" "+"))
Fiona is white.
True
1
proof
[(triple13 OR ((triple11) -> rule2))]
("Fiona" "is" "white" "+")
triple13
((triple11) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is not smart.
False
1
inv-proof
[(triple12 OR ((triple9) -> rule6) OR ((((triple11 triple14) -> rule4)) -> rule6))]
("Fiona" "is" "smart" "-")
triple12
((triple9) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((((triple11 triple14) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
@0: Dave is blue.[(triple1)] Dave is cold.[(triple2)] Dave is kind.[(triple3)] Dave is not young.[(triple7)] Dave is quiet.[(triple4)] Dave is smart.[(triple5)] Dave is white.[(triple6 OR ((triple4) -> rule2))] Fiona is blue.[(triple8)] Fiona is cold.[(triple9 OR ((triple11 triple14) -> rule4))] Fiona is kind.[(triple10 OR ((triple8) -> rule5))] Fiona is quiet.[(triple11)] Fiona is smart.[(triple12 OR ((triple9) -> rule6) OR ((((triple11 triple14) -> rule4)) -> rule6))] Fiona is white.[(triple13 OR ((triple11) -> rule2))] Fiona is young.[(triple14)]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Dave is not young.
("Dave" "is" "young" "-")
triple7
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple6
((triple4) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
triple8
Fiona is cold.
("Fiona" "is" "cold" "+")
triple9
((triple11 triple14) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
triple10
((triple8) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple11
Fiona is smart.
("Fiona" "is" "smart" "+")
triple12
((triple9) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((((triple11 triple14) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
triple13
((triple11) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
triple14