Charlie is big. Charlie is cold. Charlie is green. Charlie is red. Charlie is rough. Charlie is round. Charlie is young. If someone is green then they are big. If someone is round then they are green. Green, cold people are big. Cold, red people are big. Young, round people are rough. If someone is red then they are green.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is young.
("Charlie" "is" "young" "+")
If someone is green then they are big.
((("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
If someone is round then they are green.
((("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
Green, cold people are big.
((("someone" "is" "green" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
Cold, red people are big.
((("someone" "is" "cold" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
Young, round people are rough.
((("someone" "is" "young" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
If someone is red then they are green.
((("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
Charlie is young.
True
1
proof
[(triple7)]
("Charlie" "is" "young" "+")
triple7
Charlie is not red.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "red" "-")
triple4
@0: Charlie is big.[(triple1 OR ((triple3) -> rule1) OR ((triple2 triple4) -> rule4) OR ((triple3 triple2) -> rule3) OR ((((triple4) -> rule6)) -> rule1) OR ((((triple6) -> rule2)) -> rule1) OR ((((triple4) -> rule6) triple2) -> rule3) OR ((((triple6) -> rule2) triple2) -> rule3))] Charlie is cold.[(triple2)] Charlie is green.[(triple3 OR ((triple4) -> rule6) OR ((triple6) -> rule2))] Charlie is red.[(triple4)] Charlie is rough.[(triple5 OR ((triple7 triple6) -> rule5))] Charlie is round.[(triple6)] Charlie is young.[(triple7)]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple3) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple2 triple4) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple3 triple2) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple4) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((triple4) -> (rule6 % int2)) triple2) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((triple6) -> (rule2 % int2)) triple2) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
((triple4) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((triple6) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
((triple7 triple6) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple6
Charlie is young.
("Charlie" "is" "young" "+")
triple7