Anne is cold. Anne is green. Anne is round. Anne is white. Anne is young. Bob is not big. Bob is cold. Bob is green. Bob is rough. Bob is round. Bob is not white. Bob is young. All big people are white. All big people are not cold. Round, young people are cold. If someone is round and white then they are young. Big people are young. If Bob is white and Bob is cold then Bob is not round. All young, round people are rough. All young, round people are green.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is not big.
("Bob" "is" "big" "-")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is not white.
("Bob" "is" "white" "-")
Bob is young.
("Bob" "is" "young" "+")
All big people are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
All big people are not cold.
((("someone" "is" "big" "+")) -> ("someone" "is" "cold" "-"))
Round, young people are cold.
((("someone" "is" "round" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
If someone is round and white then they are young.
((("someone" "is" "round" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "young" "+"))
Big people are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
If Bob is white and Bob is cold then Bob is not round.
((("Bob" "is" "white" "+") ("Bob" "is" "cold" "+")) -> ("Bob" "is" "round" "-"))
All young, round people are rough.
((("someone" "is" "young" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
All young, round people are green.
((("someone" "is" "young" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
Anne is green.
True
1
proof
[(triple2 OR ((triple5 triple3) -> rule8) OR ((((triple3 triple4) -> rule4) triple3) -> rule8))]
("Anne" "is" "green" "+")
triple2
((triple5 triple3) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((((triple3 triple4) -> (rule4 % int2)) triple3) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not young.
False
1
inv-proof
[(triple5 OR ((triple3 triple4) -> rule4))]
("Anne" "is" "young" "-")
triple5
((triple3 triple4) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is rough.
True
3
proof
[(((triple5 triple3) -> rule7) OR ((((triple3 triple4) -> rule4) triple3) -> rule7))]
("Anne" "is" "rough" "+")
((triple5 triple3) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((((triple3 triple4) -> (rule4 % int2)) triple3) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not rough.
False
3
inv-proof
[(((triple5 triple3) -> rule7) OR ((((triple3 triple4) -> rule4) triple3) -> rule7))]
("Anne" "is" "rough" "-")
((triple5 triple3) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((((triple3 triple4) -> (rule4 % int2)) triple3) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
@0: Anne is cold.[(triple1 OR ((triple3 triple5) -> rule3) OR ((triple3 ((triple3 triple4) -> rule4)) -> rule3))] Anne is green.[(triple2 OR ((triple5 triple3) -> rule8) OR ((((triple3 triple4) -> rule4) triple3) -> rule8))] Anne is round.[(triple3)] Anne is white.[(triple4)] Anne is young.[(triple5 OR ((triple3 triple4) -> rule4))] Bob is cold.[(triple7 OR ((triple10 triple12) -> rule3))] Bob is green.[(triple8 OR ((triple12 triple10) -> rule8))] Bob is not big.[(triple6)] Bob is not white.[(triple11)] Bob is rough.[(triple9 OR ((triple12 triple10) -> rule7))] Bob is round.[(triple10)] Bob is young.[(triple12)] @1: Anne is rough.[(((triple5 triple3) -> rule7) OR ((((triple3 triple4) -> rule4) triple3) -> rule7))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
((triple3 triple5) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((triple3 ((triple3 triple4) -> (rule4 % int2))) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
triple2
((triple5 triple3) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((((triple3 triple4) -> (rule4 % int2)) triple3) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
triple3
Anne is white.
("Anne" "is" "white" "+")
triple4
Anne is young.
("Anne" "is" "young" "+")
triple5
((triple3 triple4) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
triple7
((triple10 triple12) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
triple8
((triple12 triple10) -> (rule8 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is not big.
("Bob" "is" "big" "-")
triple6
Bob is not white.
("Bob" "is" "white" "-")
triple11
Bob is rough.
("Bob" "is" "rough" "+")
triple9
((triple12 triple10) -> (rule7 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple10
Bob is young.
("Bob" "is" "young" "+")
triple12
Anne is rough.
("Anne" "is" "rough" "+")
((triple5 triple3) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((((triple3 triple4) -> (rule4 % int2)) triple3) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2