Dave is cold. Dave is furry. Dave is green. Dave is red. Dave is rough. Dave is white. Dave is young. Fiona is cold. Fiona is not furry. Fiona is rough. Fiona is white. Fiona is young. All furry people are young. All rough people are young. If someone is green then they are red. If someone is cold then they are red. If Fiona is furry then Fiona is white. Red people are green.
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is not furry.
("Fiona" "is" "furry" "-")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Fiona is young.
("Fiona" "is" "young" "+")
All furry people are young.
((("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
All rough people are young.
((("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
If someone is green then they are red.
((("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
If someone is cold then they are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
If Fiona is furry then Fiona is white.
((("Fiona" "is" "furry" "+")) -> ("Fiona" "is" "white" "+"))
Red people are green.
((("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
Dave is green.
True
1
proof
[(triple3 OR ((triple4) -> rule6) OR ((((triple1) -> rule4)) -> rule6))]
("Dave" "is" "green" "+")
triple3
((triple4) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is not cold.
False
1
inv-proof
[(triple1)]
("Dave" "is" "cold" "-")
triple1
Fiona is red.
True
2
proof
[(((triple8) -> rule4))]
("Fiona" "is" "red" "+")
((triple8) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is not red.
False
2
inv-proof
[(((triple8) -> rule4))]
("Fiona" "is" "red" "-")
((triple8) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is green.
True
3
proof
[(((((triple8) -> rule4)) -> rule6))]
("Fiona" "is" "green" "+")
((((triple8) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is not green.
False
3
inv-proof
[(((((triple8) -> rule4)) -> rule6))]
("Fiona" "is" "green" "-")
((((triple8) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
@0: Dave is cold.[(triple1)] Dave is furry.[(triple2)] Dave is green.[(triple3 OR ((triple4) -> rule6) OR ((((triple1) -> rule4)) -> rule6))] Dave is red.[(triple4 OR ((triple1) -> rule4) OR ((triple3) -> rule3))] Dave is rough.[(triple5)] Dave is white.[(triple6)] Dave is young.[(triple7 OR ((triple2) -> rule1) OR ((triple5) -> rule2))] Fiona is cold.[(triple8)] Fiona is not furry.[(triple9)] Fiona is rough.[(triple10)] Fiona is white.[(triple11)] Fiona is young.[(triple12 OR ((triple10) -> rule2))] @1: Fiona is red.[(((triple8) -> rule4))] @2: Fiona is green.[(((((triple8) -> rule4)) -> rule6))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Dave is green.
("Dave" "is" "green" "+")
triple3
((triple4) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
triple4
((triple1) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((triple3) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
((triple2) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple5) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple8
Fiona is not furry.
("Fiona" "is" "furry" "-")
triple9
Fiona is rough.
("Fiona" "is" "rough" "+")
triple10
Fiona is white.
("Fiona" "is" "white" "+")
triple11
Fiona is young.
("Fiona" "is" "young" "+")
triple12
((triple10) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((triple8) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
((((triple8) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2