Dave is big. Dave is blue. Dave is cold. Dave is red. Dave is rough. Dave is smart. Dave is young. Erin is big. Erin is cold. Erin is rough. Erin is smart. Erin is young. All young people are blue. If Dave is big then Dave is smart. All rough people are smart. If someone is rough then they are cold. Blue, smart people are young. If someone is red and young then they are smart. Cold, blue people are young. All rough people are young.
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
All young people are blue.
((("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
If Dave is big then Dave is smart.
((("Dave" "is" "big" "+")) -> ("Dave" "is" "smart" "+"))
All rough people are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
If someone is rough then they are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
Blue, smart people are young.
((("someone" "is" "blue" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
If someone is red and young then they are smart.
((("someone" "is" "red" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
Cold, blue people are young.
((("someone" "is" "cold" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
All rough people are young.
((("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
Erin is rough.
True
1
proof
[(triple10)]
("Erin" "is" "rough" "+")
triple10
Erin is not big.
False
1
inv-proof
[(triple8)]
("Erin" "is" "big" "-")
triple8
@0: Dave is big.[(triple1)] Dave is blue.[(triple2 OR ((triple7) -> rule1) OR ((((triple5) -> rule8)) -> rule1))] Dave is cold.[(triple3 OR ((triple5) -> rule4))] Dave is red.[(triple4)] Dave is rough.[(triple5)] Dave is smart.[(triple6 OR ((triple1) -> rule2) OR ((triple5) -> rule3) OR ((triple4 triple7) -> rule6) OR ((triple4 ((triple5) -> rule8)) -> rule6) OR ((triple4 ((triple3 triple2) -> rule7)) -> rule6) OR ((triple4 ((((triple5) -> rule4) triple2) -> rule7)) -> rule6))] Dave is young.[(triple7 OR ((triple5) -> rule8) OR ((triple2 triple6) -> rule5) OR ((triple3 triple2) -> rule7) OR ((triple2 ((triple1) -> rule2)) -> rule5) OR ((triple2 ((triple5) -> rule3)) -> rule5) OR ((((triple5) -> rule4) triple2) -> rule7))] Erin is big.[(triple8)] Erin is cold.[(triple9 OR ((triple10) -> rule4))] Erin is rough.[(triple10)] Erin is smart.[(triple11 OR ((triple10) -> rule3))] Erin is young.[(triple12 OR ((triple10) -> rule8))] @1: Erin is blue.[(((triple12) -> rule1) OR ((((triple10) -> rule8)) -> rule1))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
((triple7) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple5) -> (rule8 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
triple3
((triple5) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple4
Dave is rough.
("Dave" "is" "rough" "+")
triple5
Dave is smart.
("Dave" "is" "smart" "+")
triple6
((triple1) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple5) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple4 triple7) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple4 ((triple5) -> (rule8 % int2))) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
((triple4 ((triple3 triple2) -> (rule7 % int2))) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
((triple4 ((((triple5) -> (rule4 % int3)) triple2) -> (rule7 % int2))) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
triple7
((triple5) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple2 triple6) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple3 triple2) -> (rule7 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple2 ((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((triple2 ((triple5) -> (rule3 % int2))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple5) -> (rule4 % int2)) triple2) -> (rule7 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
triple8
Erin is cold.
("Erin" "is" "cold" "+")
triple9
((triple10) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
triple10
Erin is smart.
("Erin" "is" "smart" "+")
triple11
((triple10) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
triple12
((triple10) -> (rule8 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple12) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((triple10) -> (rule8 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2