Fiona is big. Fiona is not green. Fiona is not kind. Fiona is quiet. Fiona is not round. Fiona is smart. Fiona is young. Gary is big. Gary is green. Gary is kind. Gary is quiet. Gary is round. Gary is smart. Gary is young. If Fiona is big then Fiona is quiet. If Fiona is not round then Fiona is young. All young, round things are big. If Gary is young and Gary is not big then Gary is not green. Round, quiet things are kind. All round things are kind. If something is smart and green then it is kind. If something is quiet and not big then it is kind.
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is not green.
("Fiona" "is" "green" "-")
Fiona is not kind.
("Fiona" "is" "kind" "-")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is not round.
("Fiona" "is" "round" "-")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
If Fiona is big then Fiona is quiet.
((("Fiona" "is" "big" "+")) -> ("Fiona" "is" "quiet" "+"))
If Fiona is not round then Fiona is young.
((("Fiona" "is" "round" "~")) -> ("Fiona" "is" "young" "+"))
All young, round things are big.
((("something" "is" "young" "+") ("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
If Gary is young and Gary is not big then Gary is not green.
((("Gary" "is" "young" "+") ("Gary" "is" "big" "~")) -> ("Gary" "is" "green" "-"))
Round, quiet things are kind.
((("something" "is" "round" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
All round things are kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
If something is smart and green then it is kind.
((("something" "is" "smart" "+") ("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
If something is quiet and not big then it is kind.
((("something" "is" "quiet" "+") ("something" "is" "big" "~")) -> ("something" "is" "kind" "+"))
Fiona is young.
True
1
proof
[(triple7 OR ((triple5) -> rule2))]
("Fiona" "is" "young" "+")
triple7
((triple5) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Gary is not kind.
False
1
inv-proof
[(triple10 OR ((triple12) -> rule6) OR ((triple12 triple11) -> rule5) OR ((triple13 triple9) -> rule7))]
("Gary" "is" "kind" "-")
triple10
((triple12) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple12 triple11) -> (rule5 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple13 triple9) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
@0: Fiona is big.[(triple1)] Fiona is not green.[(triple2)] Fiona is not kind.[(triple3)] Fiona is not round.[(triple5)] Fiona is quiet.[(triple4 OR ((triple1) -> rule1))] Fiona is smart.[(triple6)] Fiona is young.[(triple7 OR ((triple5) -> rule2))] Gary is big.[(triple8 OR ((triple14 triple12) -> rule3))] Gary is green.[(triple9)] Gary is kind.[(triple10 OR ((triple12) -> rule6) OR ((triple12 triple11) -> rule5) OR ((triple13 triple9) -> rule7))] Gary is quiet.[(triple11)] Gary is round.[(triple12)] Gary is smart.[(triple13)] Gary is young.[(triple14)]
Fiona is big.
("Fiona" "is" "big" "+")
triple1
Fiona is not green.
("Fiona" "is" "green" "-")
triple2
Fiona is not kind.
("Fiona" "is" "kind" "-")
triple3
Fiona is not round.
("Fiona" "is" "round" "-")
triple5
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple4
((triple1) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
triple6
Fiona is young.
("Fiona" "is" "young" "+")
triple7
((triple5) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
triple8
((triple14 triple12) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
triple9
Gary is kind.
("Gary" "is" "kind" "+")
triple10
((triple12) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple12 triple11) -> (rule5 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple13 triple9) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
triple11
Gary is round.
("Gary" "is" "round" "+")
triple12
Gary is smart.
("Gary" "is" "smart" "+")
triple13
Gary is young.
("Gary" "is" "young" "+")
triple14