Fiona is quiet. Fiona is red. Fiona is rough. If something is big then it is young. If something is quiet then it is young. All red, young things are quiet. All quiet things are red. If Fiona is red and Fiona is big then Fiona is kind. All rough things are furry. Red, young things are big. Furry things are rough.
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
If something is big then it is young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If something is quiet then it is young.
((("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
All red, young things are quiet.
((("something" "is" "red" "+") ("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
All quiet things are red.
((("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
If Fiona is red and Fiona is big then Fiona is kind.
((("Fiona" "is" "red" "+") ("Fiona" "is" "big" "+")) -> ("Fiona" "is" "kind" "+"))
All rough things are furry.
((("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
Red, young things are big.
((("something" "is" "red" "+") ("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
Furry things are rough.
((("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
Fiona is red.
True
1
proof
[(triple2 OR ((triple1) -> rule4))]
("Fiona" "is" "red" "+")
triple2
((triple1) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is not quiet.
False
1
inv-proof
[(triple1)]
("Fiona" "is" "quiet" "-")
triple1
Fiona is young.
True
2
proof
[(((triple1) -> rule2))]
("Fiona" "is" "young" "+")
((triple1) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is not furry.
False
2
inv-proof
[(((triple3) -> rule6))]
("Fiona" "is" "furry" "-")
((triple3) -> (rule6 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is big.
True
4
proof
[(((triple2 ((triple1) -> rule2)) -> rule7) OR ((((triple1) -> rule4) ((triple1) -> rule2)) -> rule7))]
("Fiona" "is" "big" "+")
((triple2 ((triple1) -> (rule2 % int2))) -> (rule7 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((((triple1) -> (rule4 % int3)) ((triple1) -> (rule2 % int2))) -> (rule7 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is not big.
False
4
inv-proof
[(((triple2 ((triple1) -> rule2)) -> rule7) OR ((((triple1) -> rule4) ((triple1) -> rule2)) -> rule7))]
("Fiona" "is" "big" "-")
((triple2 ((triple1) -> (rule2 % int2))) -> (rule7 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((((triple1) -> (rule4 % int3)) ((triple1) -> (rule2 % int2))) -> (rule7 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is kind.
True
6
proof
[(((triple2 ((triple2 ((triple1) -> rule2)) -> rule7)) -> rule5) OR ((triple2 ((((triple1) -> rule4) ((triple1) -> rule2)) -> rule7)) -> rule5) OR ((((triple1) -> rule4) ((triple2 ((triple1) -> rule2)) -> rule7)) -> rule5) OR ((((triple1) -> rule4) ((((triple1) -> rule4) ((triple1) -> rule2)) -> rule7)) -> rule5))]
("Fiona" "is" "kind" "+")
((triple2 ((triple2 ((triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
((triple2 ((((triple1) -> (rule4 % int4)) ((triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
((((triple1) -> (rule4 % int4)) ((triple2 ((triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
((((triple1) -> (rule4 % int4)) ((((triple1) -> (rule4 % int4)) ((triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
Fiona is not kind.
False
6
inv-proof
[(((triple2 ((triple2 ((triple1) -> rule2)) -> rule7)) -> rule5) OR ((triple2 ((((triple1) -> rule4) ((triple1) -> rule2)) -> rule7)) -> rule5) OR ((((triple1) -> rule4) ((triple2 ((triple1) -> rule2)) -> rule7)) -> rule5) OR ((((triple1) -> rule4) ((((triple1) -> rule4) ((triple1) -> rule2)) -> rule7)) -> rule5))]
("Fiona" "is" "kind" "-")
((triple2 ((triple2 ((triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
((triple2 ((((triple1) -> (rule4 % int4)) ((triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
((((triple1) -> (rule4 % int4)) ((triple2 ((triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
((((triple1) -> (rule4 % int4)) ((((triple1) -> (rule4 % int4)) ((triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
@0: Fiona is quiet.[(triple1)] Fiona is red.[(triple2 OR ((triple1) -> rule4))] Fiona is rough.[(triple3)] @1: Fiona is furry.[(((triple3) -> rule6))] Fiona is young.[(((triple1) -> rule2))] @2: Fiona is big.[(((triple2 ((triple1) -> rule2)) -> rule7) OR ((((triple1) -> rule4) ((triple1) -> rule2)) -> rule7))] @3: Fiona is kind.[(((triple2 ((triple2 ((triple1) -> rule2)) -> rule7)) -> rule5) OR ((triple2 ((((triple1) -> rule4) ((triple1) -> rule2)) -> rule7)) -> rule5) OR ((((triple1) -> rule4) ((triple2 ((triple1) -> rule2)) -> rule7)) -> rule5) OR ((((triple1) -> rule4) ((((triple1) -> rule4) ((triple1) -> rule2)) -> rule7)) -> rule5))]
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple1
Fiona is red.
("Fiona" "is" "red" "+")
triple2
((triple1) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
triple3
Fiona is furry.
("Fiona" "is" "furry" "+")
((triple3) -> (rule6 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((triple1) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple2 ((triple1) -> (rule2 % int2))) -> (rule7 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((((triple1) -> (rule4 % int3)) ((triple1) -> (rule2 % int2))) -> (rule7 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple2 ((triple2 ((triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
((triple2 ((((triple1) -> (rule4 % int4)) ((triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
((((triple1) -> (rule4 % int4)) ((triple2 ((triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
((((triple1) -> (rule4 % int4)) ((((triple1) -> (rule4 % int4)) ((triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4