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