Charlie is big. Charlie is cold. Charlie is nice. Charlie is red. Charlie is rough. Charlie is round. Charlie is young. If Charlie is rough and Charlie is big then Charlie is red. Rough, young things are big. If something is rough and nice then it is cold. If Charlie is nice then Charlie is round. All young, nice things are round. Young, nice things are big.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
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 Charlie is rough and Charlie is big then Charlie is red.
((("Charlie" "is" "rough" "+") ("Charlie" "is" "big" "+")) -> ("Charlie" "is" "red" "+"))
Rough, young things are big.
((("something" "is" "rough" "+") ("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
If something is rough and nice then it is cold.
((("something" "is" "rough" "+") ("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If Charlie is nice then Charlie is round.
((("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "round" "+"))
All young, nice things are round.
((("something" "is" "young" "+") ("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
Young, nice things are big.
((("something" "is" "young" "+") ("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
Charlie is rough.
True
1
proof
[(triple5)]
("Charlie" "is" "rough" "+")
triple5
Charlie is not big.
False
1
inv-proof
[(triple1 OR ((triple5 triple7) -> rule2) OR ((triple7 triple3) -> rule6))]
("Charlie" "is" "big" "-")
triple1
((triple5 triple7) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple7 triple3) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
@0: Charlie is big.[(triple1 OR ((triple5 triple7) -> rule2) OR ((triple7 triple3) -> rule6))] Charlie is cold.[(triple2 OR ((triple5 triple3) -> rule3))] Charlie is nice.[(triple3)] Charlie is red.[(triple4 OR ((triple5 triple1) -> rule1) OR ((triple5 ((triple5 triple7) -> rule2)) -> rule1) OR ((triple5 ((triple7 triple3) -> rule6)) -> rule1))] Charlie is rough.[(triple5)] Charlie is round.[(triple6 OR ((triple3) -> rule4) OR ((triple7 triple3) -> rule5))] Charlie is young.[(triple7)]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple5 triple7) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple7 triple3) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
((triple5 triple3) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple4
((triple5 triple1) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((triple5 ((triple5 triple7) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((triple5 ((triple7 triple3) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
Charlie is round.
("Charlie" "is" "round" "+")
triple6
((triple3) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((triple7 triple3) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
triple7