Dave is cold. Dave is furry. Dave is nice. Dave is not rough. Dave is smart. Dave is not white. Dave is young. Erin is cold. Erin is furry. Erin is nice. Erin is rough. Erin is smart. Erin is white. Erin is young. If something is nice and rough then it is cold. Nice things are cold. All smart, cold things are nice. If something is young then it is nice. Cold things are smart. If something is young and not nice then it is not furry.
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is not rough.
("Dave" "is" "rough" "-")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is not white.
("Dave" "is" "white" "-")
Dave is young.
("Dave" "is" "young" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
If something is nice and rough then it is cold.
((("something" "is" "nice" "+") ("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
Nice things are cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
All smart, cold things are nice.
((("something" "is" "smart" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If something is young then it is nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
Cold things are smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
If something is young and not nice then it is not furry.
((("something" "is" "young" "+") ("something" "is" "nice" "~")) -> ("something" "is" "furry" "-"))
Dave is young.
True
1
proof
[(triple7)]
("Dave" "is" "young" "+")
triple7
Erin is not cold.
False
1
inv-proof
[(triple8 OR ((triple10) -> rule2) OR ((triple10 triple11) -> rule1) OR ((((triple14) -> rule4)) -> rule2) OR ((((triple14) -> rule4) triple11) -> rule1))]
("Erin" "is" "cold" "-")
triple8
((triple10) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple10 triple11) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple14) -> (rule4 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((((triple14) -> (rule4 % int2)) triple11) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
@0: Dave is cold.[(triple1 OR ((triple3) -> rule2) OR ((((triple7) -> rule4)) -> rule2))] Dave is furry.[(triple2)] Dave is nice.[(triple3 OR ((triple7) -> rule4) OR ((triple5 triple1) -> rule3) OR ((((triple1) -> rule5) triple1) -> rule3))] Dave is not rough.[(triple4)] Dave is not white.[(triple6)] Dave is smart.[(triple5 OR ((triple1) -> rule5) OR ((((triple3) -> rule2)) -> rule5) OR ((((((triple7) -> rule4)) -> rule2)) -> rule5))] Dave is young.[(triple7)] Erin is cold.[(triple8 OR ((triple10) -> rule2) OR ((triple10 triple11) -> rule1) OR ((((triple14) -> rule4)) -> rule2) OR ((((triple14) -> rule4) triple11) -> rule1))] Erin is furry.[(triple9)] Erin is nice.[(triple10 OR ((triple14) -> rule4) OR ((triple12 triple8) -> rule3) OR ((((triple8) -> rule5) triple8) -> rule3))] Erin is rough.[(triple11)] Erin is smart.[(triple12 OR ((triple8) -> rule5) OR ((((triple10) -> rule2)) -> rule5) OR ((((triple10 triple11) -> rule1)) -> rule5) OR ((((((triple14) -> rule4)) -> rule2)) -> rule5) OR ((((((triple14) -> rule4) triple11) -> rule1)) -> rule5))] Erin is white.[(triple13)] Erin is young.[(triple14)]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
((triple3) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((triple7) -> (rule4 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
((triple7) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple5 triple1) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple1) -> (rule5 % int2)) triple1) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is not rough.
("Dave" "is" "rough" "-")
triple4
Dave is not white.
("Dave" "is" "white" "-")
triple6
Dave is smart.
("Dave" "is" "smart" "+")
triple5
((triple1) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
((((((triple7) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
triple7
Erin is cold.
("Erin" "is" "cold" "+")
triple8
((triple10) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple10 triple11) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple14) -> (rule4 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((((triple14) -> (rule4 % int2)) triple11) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
triple9
Erin is nice.
("Erin" "is" "nice" "+")
triple10
((triple14) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((triple12 triple8) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((((triple8) -> (rule5 % int2)) triple8) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
triple11
Erin is smart.
("Erin" "is" "smart" "+")
triple12
((triple8) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple10) -> (rule2 % int2))) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((triple10 triple11) -> (rule1 % int2))) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((((triple14) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
((((((triple14) -> (rule4 % int3)) triple11) -> (rule1 % int2))) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
triple13
Erin is young.
("Erin" "is" "young" "+")
triple14