Fiona is big. Fiona is green. Fiona is quiet. Fiona is red. Fiona is rough. Fiona is round. Fiona is young. All round things are young. All quiet things are rough. If Fiona is young and Fiona is rough then Fiona is red. All green things are young. If something is young then it is big. Red things are big.
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is young.
("Fiona" "is" "young" "+")
All round things are young.
((("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
All quiet things are rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
If Fiona is young and Fiona is rough then Fiona is red.
((("Fiona" "is" "young" "+") ("Fiona" "is" "rough" "+")) -> ("Fiona" "is" "red" "+"))
All green things are young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
If something is young then it is big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
Red things are big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
Fiona is red.
True
1
proof
[(triple4 OR ((triple7 triple5) -> rule3) OR ((triple7 ((triple3) -> rule2)) -> rule3) OR ((((triple2) -> rule4) triple5) -> rule3) OR ((((triple6) -> rule1) triple5) -> rule3) OR ((((triple2) -> rule4) ((triple3) -> rule2)) -> rule3) OR ((((triple6) -> rule1) ((triple3) -> rule2)) -> rule3))]
("Fiona" "is" "red" "+")
triple4
((triple7 triple5) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((triple7 ((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
((((triple2) -> (rule4 % int2)) triple5) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((((triple6) -> (rule1 % int2)) triple5) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((((triple2) -> (rule4 % int3)) ((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
((((triple6) -> (rule1 % int3)) ((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is not young.
False
1
inv-proof
[(triple7 OR ((triple2) -> rule4) OR ((triple6) -> rule1))]
("Fiona" "is" "young" "-")
triple7
((triple2) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((triple6) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
@0: Fiona is big.[(triple1 OR ((triple4) -> rule6) OR ((triple7) -> rule5) OR ((((triple2) -> rule4)) -> rule5) OR ((((triple6) -> rule1)) -> rule5) OR ((((triple7 triple5) -> rule3)) -> rule6) OR ((((triple7 ((triple3) -> rule2)) -> rule3)) -> rule6) OR ((((((triple2) -> rule4) triple5) -> rule3)) -> rule6) OR ((((((triple6) -> rule1) triple5) -> rule3)) -> rule6) OR ((((((triple2) -> rule4) ((triple3) -> rule2)) -> rule3)) -> rule6) OR ((((((triple6) -> rule1) ((triple3) -> rule2)) -> rule3)) -> rule6))] Fiona is green.[(triple2)] Fiona is quiet.[(triple3)] Fiona is red.[(triple4 OR ((triple7 triple5) -> rule3) OR ((triple7 ((triple3) -> rule2)) -> rule3) OR ((((triple2) -> rule4) triple5) -> rule3) OR ((((triple6) -> rule1) triple5) -> rule3) OR ((((triple2) -> rule4) ((triple3) -> rule2)) -> rule3) OR ((((triple6) -> rule1) ((triple3) -> rule2)) -> rule3))] Fiona is rough.[(triple5 OR ((triple3) -> rule2))] Fiona is round.[(triple6)] Fiona is young.[(triple7 OR ((triple2) -> rule4) OR ((triple6) -> rule1))]
Fiona is big.
("Fiona" "is" "big" "+")
triple1
((triple4) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((triple7) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((((triple6) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((((triple7 triple5) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
((((triple7 ((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
((((((triple2) -> (rule4 % int3)) triple5) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
((((((triple6) -> (rule1 % int3)) triple5) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
((((((triple2) -> (rule4 % int4)) ((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is young.
("Fiona" "is" "young" "+")
int4
((((((triple6) -> (rule1 % int4)) ((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is young.
("Fiona" "is" "young" "+")
int4
Fiona is green.
("Fiona" "is" "green" "+")
triple2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple3
Fiona is red.
("Fiona" "is" "red" "+")
triple4
((triple7 triple5) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((triple7 ((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
((((triple2) -> (rule4 % int2)) triple5) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((((triple6) -> (rule1 % int2)) triple5) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((((triple2) -> (rule4 % int3)) ((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
((((triple6) -> (rule1 % int3)) ((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
triple5
((triple3) -> (rule2 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
triple6
Fiona is young.
("Fiona" "is" "young" "+")
triple7
((triple2) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((triple6) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1