Charlie is blue. Charlie is rough. Charlie is round. Fiona is big. Fiona is blue. Fiona is kind. Fiona is quiet. Fiona is rough. Fiona is round. Fiona is young. Gary is blue. Gary is kind. Gary is quiet. Gary is rough. Gary is round. Gary is young. All quiet, big things are young. All blue, young things are quiet. If Charlie is quiet and Charlie is round then Charlie is big. All kind things are big. Blue things are quiet. If Charlie is big and Charlie is quiet then Charlie is round.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is young.
("Gary" "is" "young" "+")
All quiet, big things are young.
((("something" "is" "quiet" "+") ("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
All blue, young things are quiet.
((("something" "is" "blue" "+") ("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
If Charlie is quiet and Charlie is round then Charlie is big.
((("Charlie" "is" "quiet" "+") ("Charlie" "is" "round" "+")) -> ("Charlie" "is" "big" "+"))
All kind things are big.
((("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
Blue things are quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
If Charlie is big and Charlie is quiet then Charlie is round.
((("Charlie" "is" "big" "+") ("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "round" "+"))
Gary is quiet.
True
1
proof
[(triple13 OR ((triple11) -> rule5) OR ((triple11 triple16) -> rule2))]
("Gary" "is" "quiet" "+")
triple13
((triple11) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((triple11 triple16) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Fiona is not big.
False
1
inv-proof
[(triple4 OR ((triple6) -> rule4))]
("Fiona" "is" "big" "-")
triple4
((triple6) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Charlie is quiet.
True
2
proof
[(((triple1) -> rule5))]
("Charlie" "is" "quiet" "+")
((triple1) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is not quiet.
False
2
inv-proof
[(((triple1) -> rule5))]
("Charlie" "is" "quiet" "-")
((triple1) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is big.
True
4
proof
[(((((triple1) -> rule5) triple3) -> rule3))]
("Charlie" "is" "big" "+")
((((triple1) -> (rule5 % int2)) triple3) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not big.
False
4
inv-proof
[(((((triple1) -> rule5) triple3) -> rule3))]
("Charlie" "is" "big" "-")
((((triple1) -> (rule5 % int2)) triple3) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is young.
True
7
proof
[(((((triple1) -> rule5) ((((triple1) -> rule5) triple3) -> rule3)) -> rule1))]
("Charlie" "is" "young" "+")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3)) triple3) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is not young.
False
7
inv-proof
[(((((triple1) -> rule5) ((((triple1) -> rule5) triple3) -> rule3)) -> rule1))]
("Charlie" "is" "young" "-")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3)) triple3) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
@0: Charlie is blue.[(triple1)] Charlie is rough.[(triple2)] Charlie is round.[(triple3)] Fiona is big.[(triple4 OR ((triple6) -> rule4))] Fiona is blue.[(triple5)] Fiona is kind.[(triple6)] Fiona is quiet.[(triple7 OR ((triple5) -> rule5) OR ((triple5 triple10) -> rule2))] Fiona is rough.[(triple8)] Fiona is round.[(triple9)] Fiona is young.[(triple10 OR ((triple7 triple4) -> rule1) OR ((triple7 ((triple6) -> rule4)) -> rule1) OR ((((triple5) -> rule5) triple4) -> rule1) OR ((((triple5) -> rule5) ((triple6) -> rule4)) -> rule1))] Gary is blue.[(triple11)] Gary is kind.[(triple12)] Gary is quiet.[(triple13 OR ((triple11) -> rule5) OR ((triple11 triple16) -> rule2))] Gary is rough.[(triple14)] Gary is round.[(triple15)] Gary is young.[(triple16 OR ((triple13 ((triple12) -> rule4)) -> rule1) OR ((((triple11) -> rule5) ((triple12) -> rule4)) -> rule1))] @1: Charlie is quiet.[(((triple1) -> rule5))] Gary is big.[(((triple12) -> rule4))] @2: Charlie is big.[(((((triple1) -> rule5) triple3) -> rule3))] @3: Charlie is young.[(((((triple1) -> rule5) ((((triple1) -> rule5) triple3) -> rule3)) -> rule1))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Charlie is round.
("Charlie" "is" "round" "+")
triple3
Fiona is big.
("Fiona" "is" "big" "+")
triple4
((triple6) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
triple5
Fiona is kind.
("Fiona" "is" "kind" "+")
triple6
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple7
((triple5) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((triple5 triple10) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
triple8
Fiona is round.
("Fiona" "is" "round" "+")
triple9
Fiona is young.
("Fiona" "is" "young" "+")
triple10
((triple7 triple4) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((triple7 ((triple6) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
((((triple5) -> (rule5 % int2)) triple4) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
((((triple5) -> (rule5 % int3)) ((triple6) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
triple11
Gary is kind.
("Gary" "is" "kind" "+")
triple12
Gary is quiet.
("Gary" "is" "quiet" "+")
triple13
((triple11) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((triple11 triple16) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
triple14
Gary is round.
("Gary" "is" "round" "+")
triple15
Gary is young.
("Gary" "is" "young" "+")
triple16
((triple13 ((triple12) -> (rule4 % int2))) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((triple11) -> (rule5 % int3)) ((triple12) -> (rule4 % int2))) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple1) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple12) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((((triple1) -> (rule5 % int2)) triple3) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3)) triple3) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3