Dave is not big. Dave is not nice. Dave is quiet. Dave is round. Dave is smart. Dave is not white. Dave is not young. Fiona is round. Fiona is young. Gary is not big. Gary is nice. Gary is quiet. Gary is not round. Gary is smart. Gary is white. Gary is young. If something is round and big then it is not smart. If Fiona is big then Fiona is quiet. If Fiona is young then Fiona is big. If something is nice and not young then it is round. All big things are round. If something is quiet and big then it is white. If Dave is young then Dave is not round. White, smart things are quiet.
Dave is not big.
("Dave" "is" "big" "-")
Dave is not nice.
("Dave" "is" "nice" "-")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is not white.
("Dave" "is" "white" "-")
Dave is not young.
("Dave" "is" "young" "-")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is not big.
("Gary" "is" "big" "-")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is not round.
("Gary" "is" "round" "-")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
If something is round and big then it is not smart.
((("something" "is" "round" "+") ("something" "is" "big" "+")) -> ("something" "is" "smart" "-"))
If Fiona is big then Fiona is quiet.
((("Fiona" "is" "big" "+")) -> ("Fiona" "is" "quiet" "+"))
If Fiona is young then Fiona is big.
((("Fiona" "is" "young" "+")) -> ("Fiona" "is" "big" "+"))
If something is nice and not young then it is round.
((("something" "is" "nice" "+") ("something" "is" "young" "~")) -> ("something" "is" "round" "+"))
All big things are round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
If something is quiet and big then it is white.
((("something" "is" "quiet" "+") ("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
If Dave is young then Dave is not round.
((("Dave" "is" "young" "+")) -> ("Dave" "is" "round" "-"))
White, smart things are quiet.
((("something" "is" "white" "+") ("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
Gary is not big.
True
1
proof
[(triple10)]
("Gary" "is" "big" "-")
triple10
Dave is young.
False
1
inv-proof
[(triple7)]
("Dave" "is" "young" "+")
triple7
Fiona is big.
True
2
proof
[(((triple9) -> rule3))]
("Fiona" "is" "big" "+")
((triple9) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is not big.
False
2
inv-proof
[(((triple9) -> rule3))]
("Fiona" "is" "big" "-")
((triple9) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is not smart.
True
4
proof
[(((triple8 ((triple9) -> rule3)) -> rule1) OR ((((((triple9) -> rule3)) -> rule5) ((triple9) -> rule3)) -> rule1))]
("Fiona" "is" "smart" "-")
((triple8 ((triple9) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is not smart.
("Fiona" "is" "smart" "-")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
((((((triple9) -> (rule3 % int3))) -> (rule5 % int2)) ((triple9) -> (rule3 % int3))) -> (rule1 % int1))
Fiona is not smart.
("Fiona" "is" "smart" "-")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is smart.
False
4
inv-proof
[(((triple8 ((triple9) -> rule3)) -> rule1) OR ((((((triple9) -> rule3)) -> rule5) ((triple9) -> rule3)) -> rule1))]
("Fiona" "is" "smart" "+")
((triple8 ((triple9) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is not smart.
("Fiona" "is" "smart" "-")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
((((((triple9) -> (rule3 % int3))) -> (rule5 % int2)) ((triple9) -> (rule3 % int3))) -> (rule1 % int1))
Fiona is not smart.
("Fiona" "is" "smart" "-")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is white.
True
6
proof
[(((((((triple9) -> rule3)) -> rule2) ((triple9) -> rule3)) -> rule6))]
("Fiona" "is" "white" "+")
((((((triple9) -> (rule3 % int3))) -> (rule2 % int2)) ((triple9) -> (rule3 % int3))) -> (rule6 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is not white.
False
6
inv-proof
[(((((((triple9) -> rule3)) -> rule2) ((triple9) -> rule3)) -> rule6))]
("Fiona" "is" "white" "-")
((((((triple9) -> (rule3 % int3))) -> (rule2 % int2)) ((triple9) -> (rule3 % int3))) -> (rule6 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
@0: Dave is not big.[(triple1)] Dave is not nice.[(triple2)] Dave is not white.[(triple6)] Dave is not young.[(triple7)] Dave is quiet.[(triple3)] Dave is round.[(triple4)] Dave is smart.[(triple5)] Fiona is round.[(triple8 OR ((((triple9) -> rule3)) -> rule5))] Fiona is young.[(triple9)] Gary is nice.[(triple11)] Gary is not big.[(triple10)] Gary is not round.[(triple13)] Gary is quiet.[(triple12 OR ((triple15 triple14) -> rule8))] Gary is smart.[(triple14)] Gary is white.[(triple15)] Gary is young.[(triple16)] @1: Fiona is big.[(((triple9) -> rule3))] @2: Fiona is not smart.[(((triple8 ((triple9) -> rule3)) -> rule1) OR ((((((triple9) -> rule3)) -> rule5) ((triple9) -> rule3)) -> rule1))] Fiona is quiet.[(((((triple9) -> rule3)) -> rule2))] @3: Fiona is white.[(((((((triple9) -> rule3)) -> rule2) ((triple9) -> rule3)) -> rule6))]
Dave is not big.
("Dave" "is" "big" "-")
triple1
Dave is not nice.
("Dave" "is" "nice" "-")
triple2
Dave is not white.
("Dave" "is" "white" "-")
triple6
Dave is not young.
("Dave" "is" "young" "-")
triple7
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Dave is round.
("Dave" "is" "round" "+")
triple4
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Fiona is round.
("Fiona" "is" "round" "+")
triple8
((((triple9) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
triple9
Gary is nice.
("Gary" "is" "nice" "+")
triple11
Gary is not big.
("Gary" "is" "big" "-")
triple10
Gary is not round.
("Gary" "is" "round" "-")
triple13
Gary is quiet.
("Gary" "is" "quiet" "+")
triple12
((triple15 triple14) -> (rule8 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple14
Gary is white.
("Gary" "is" "white" "+")
triple15
Gary is young.
("Gary" "is" "young" "+")
triple16
Fiona is big.
("Fiona" "is" "big" "+")
((triple9) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is not smart.
("Fiona" "is" "smart" "-")
((triple8 ((triple9) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is not smart.
("Fiona" "is" "smart" "-")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
((((((triple9) -> (rule3 % int3))) -> (rule5 % int2)) ((triple9) -> (rule3 % int3))) -> (rule1 % int1))
Fiona is not smart.
("Fiona" "is" "smart" "-")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((triple9) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
((((((triple9) -> (rule3 % int3))) -> (rule2 % int2)) ((triple9) -> (rule3 % int3))) -> (rule6 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3