Charlie is furry. Charlie is kind. Charlie is smart. Fiona is big. Fiona is furry. Fiona is smart. Fiona is young. Young things are quiet. All quiet things are furry. Red, big things are quiet. All red, kind things are young. Kind things are big. Kind, red things are quiet. Smart things are red. If something is smart then it is big.
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Young things are quiet.
((("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
All quiet things are furry.
((("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
Red, big things are quiet.
((("something" "is" "red" "+") ("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
All red, kind things are young.
((("something" "is" "red" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
Kind things are big.
((("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
Kind, red things are quiet.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
Smart things are red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
If something is smart then it is big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
Fiona is furry.
True
1
proof
[(triple5 OR ((((triple7) -> rule1)) -> rule2) OR ((((((triple6) -> rule7) triple4) -> rule3)) -> rule2) OR ((((((triple6) -> rule7) ((triple6) -> rule8)) -> rule3)) -> rule2))]
("Fiona" "is" "furry" "+")
triple5
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
((((((triple6) -> (rule7 % int3)) triple4) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
((((((triple6) -> (rule7 % int4)) ((triple6) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
Charlie is not smart.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "smart" "-")
triple3
Charlie is big.
True
2
proof
[(((triple2) -> rule5) OR ((triple3) -> rule8))]
("Charlie" "is" "big" "+")
((triple2) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple3) -> (rule8 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not red.
False
2
inv-proof
[(((triple3) -> rule7))]
("Charlie" "is" "red" "-")
((triple3) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
@0: Charlie is furry.[(triple1 OR ((((triple2 ((triple3) -> rule7)) -> rule6)) -> rule2) OR ((((((triple3) -> rule7) ((triple2) -> rule5)) -> rule3)) -> rule2) OR ((((((triple3) -> rule7) ((triple3) -> rule8)) -> rule3)) -> rule2) OR ((((((((triple3) -> rule7) triple2) -> rule4)) -> rule1)) -> rule2))] Charlie is kind.[(triple2)] Charlie is smart.[(triple3)] Fiona is big.[(triple4 OR ((triple6) -> rule8))] Fiona is furry.[(triple5 OR ((((triple7) -> rule1)) -> rule2) OR ((((((triple6) -> rule7) triple4) -> rule3)) -> rule2) OR ((((((triple6) -> rule7) ((triple6) -> rule8)) -> rule3)) -> rule2))] Fiona is smart.[(triple6)] Fiona is young.[(triple7)] @1: Charlie is big.[(((triple2) -> rule5) OR ((triple3) -> rule8))] Charlie is red.[(((triple3) -> rule7))] Fiona is quiet.[(((triple7) -> rule1) OR ((((triple6) -> rule7) triple4) -> rule3) OR ((((triple6) -> rule7) ((triple6) -> rule8)) -> rule3))] Fiona is red.[(((triple6) -> rule7))] @2: Charlie is quiet.[(((triple2 ((triple3) -> rule7)) -> rule6) OR ((((triple3) -> rule7) ((triple2) -> rule5)) -> rule3) OR ((((triple3) -> rule7) ((triple3) -> rule8)) -> rule3) OR ((((((triple3) -> rule7) triple2) -> rule4)) -> rule1))] Charlie is young.[(((((triple3) -> rule7) triple2) -> rule4))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
((((triple2 ((triple3) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
((((((triple3) -> (rule7 % int4)) ((triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
int4
((((((triple3) -> (rule7 % int4)) ((triple3) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
int4
((((((((triple3) -> (rule7 % int4)) triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
int4
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
Fiona is big.
("Fiona" "is" "big" "+")
triple4
((triple6) -> (rule8 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
triple5
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
((((((triple6) -> (rule7 % int3)) triple4) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
((((((triple6) -> (rule7 % int4)) ((triple6) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
Fiona is smart.
("Fiona" "is" "smart" "+")
triple6
Fiona is young.
("Fiona" "is" "young" "+")
triple7
Charlie is big.
("Charlie" "is" "big" "+")
((triple2) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple3) -> (rule8 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((triple3) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple7) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((((triple6) -> (rule7 % int2)) triple4) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
((((triple6) -> (rule7 % int3)) ((triple6) -> (rule8 % int2))) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
((triple6) -> (rule7 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple2 ((triple3) -> (rule7 % int2))) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
((((triple3) -> (rule7 % int3)) ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
((((triple3) -> (rule7 % int3)) ((triple3) -> (rule8 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
((((((triple3) -> (rule7 % int3)) triple2) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
((((triple3) -> (rule7 % int2)) triple2) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2