Charlie is big. Charlie is cold. Charlie is nice. Charlie is rough. Charlie is round. Charlie is smart. Charlie is young. Fiona is not big. Fiona is cold. Fiona is nice. Fiona is rough. Fiona is round. Fiona is smart. Fiona is not young. If someone is smart then they are rough. All young, smart people are cold. If Charlie is cold and Charlie is smart then Charlie is round. If someone is rough then they are round. If someone is cold and not rough then they are round. If Fiona is not round then Fiona is not nice.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Fiona is not big.
("Fiona" "is" "big" "-")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is not young.
("Fiona" "is" "young" "-")
If someone is smart then they are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
All young, smart people are cold.
((("someone" "is" "young" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
If Charlie is cold and Charlie is smart then Charlie is round.
((("Charlie" "is" "cold" "+") ("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "round" "+"))
If someone is rough then they are round.
((("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
If someone is cold and not rough then they are round.
((("someone" "is" "cold" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "round" "+"))
If Fiona is not round then Fiona is not nice.
((("Fiona" "is" "round" "~")) -> ("Fiona" "is" "nice" "-"))
Charlie is round.
True
1
proof
[(triple5 OR ((triple4) -> rule4) OR ((triple2 triple6) -> rule3) OR ((((triple6) -> rule1)) -> rule4) OR ((((triple7 triple6) -> rule2) triple6) -> rule3))]
("Charlie" "is" "round" "+")
triple5
((triple4) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((triple2 triple6) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((triple6) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((triple7 triple6) -> (rule2 % int2)) triple6) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Fiona is big.
False
1
inv-proof
[(triple8)]
("Fiona" "is" "big" "+")
triple8
@0: Charlie is big.[(triple1)] Charlie is cold.[(triple2 OR ((triple7 triple6) -> rule2))] Charlie is nice.[(triple3)] Charlie is rough.[(triple4 OR ((triple6) -> rule1))] Charlie is round.[(triple5 OR ((triple4) -> rule4) OR ((triple2 triple6) -> rule3) OR ((((triple6) -> rule1)) -> rule4) OR ((((triple7 triple6) -> rule2) triple6) -> rule3))] Charlie is smart.[(triple6)] Charlie is young.[(triple7)] Fiona is cold.[(triple9)] Fiona is nice.[(triple10)] Fiona is not big.[(triple8)] Fiona is not young.[(triple14)] Fiona is rough.[(triple11 OR ((triple13) -> rule1))] Fiona is round.[(triple12 OR ((triple11) -> rule4) OR ((((triple13) -> rule1)) -> rule4))] Fiona is smart.[(triple13)]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
((triple7 triple6) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is rough.
("Charlie" "is" "rough" "+")
triple4
((triple6) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple5
((triple4) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((triple2 triple6) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((triple6) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((triple7 triple6) -> (rule2 % int2)) triple6) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
Charlie is young.
("Charlie" "is" "young" "+")
triple7
Fiona is cold.
("Fiona" "is" "cold" "+")
triple9
Fiona is nice.
("Fiona" "is" "nice" "+")
triple10
Fiona is not big.
("Fiona" "is" "big" "-")
triple8
Fiona is not young.
("Fiona" "is" "young" "-")
triple14
Fiona is rough.
("Fiona" "is" "rough" "+")
triple11
((triple13) -> (rule1 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
triple12
((triple11) -> (rule4 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((((triple13) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
triple13