Bob is green. Bob is nice. Bob is quiet. Bob is round. Bob is young. Erin is green. Erin is kind. Erin is nice. Erin is quiet. Erin is round. Erin is young. Gary is kind. Gary is nice. Gary is quiet. Gary is round. If Bob is green then Bob is kind. All green things are smart. Young things are smart. If something is kind and round then it is quiet. All quiet things are young. All kind, quiet things are round. If Erin is nice and Erin is green then Erin is kind. All kind things are green.
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is round.
("Gary" "is" "round" "+")
If Bob is green then Bob is kind.
((("Bob" "is" "green" "+")) -> ("Bob" "is" "kind" "+"))
All green things are smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
Young things are smart.
((("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
If something is kind and round then it is quiet.
((("something" "is" "kind" "+") ("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
All quiet things are young.
((("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
All kind, quiet things are round.
((("something" "is" "kind" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
If Erin is nice and Erin is green then Erin is kind.
((("Erin" "is" "nice" "+") ("Erin" "is" "green" "+")) -> ("Erin" "is" "kind" "+"))
All kind things are green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
Bob is young.
True
1
proof
[(triple5 OR ((triple3) -> rule5) OR ((((((triple1) -> rule1) triple4) -> rule4)) -> rule5))]
("Bob" "is" "young" "+")
triple5
((triple3) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((((((triple1) -> (rule1 % int3)) triple4) -> (rule4 % int2))) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Erin is not green.
False
1
inv-proof
[(triple6 OR ((triple7) -> rule8))]
("Erin" "is" "green" "-")
triple6
((triple7) -> (rule8 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
@0: Bob is green.[(triple1)] Bob is nice.[(triple2)] Bob is quiet.[(triple3 OR ((((triple1) -> rule1) triple4) -> rule4))] Bob is round.[(triple4 OR ((((triple1) -> rule1) triple3) -> rule6))] Bob is young.[(triple5 OR ((triple3) -> rule5) OR ((((((triple1) -> rule1) triple4) -> rule4)) -> rule5))] Erin is green.[(triple6 OR ((triple7) -> rule8))] Erin is kind.[(triple7 OR ((triple8 triple6) -> rule7))] Erin is nice.[(triple8)] Erin is quiet.[(triple9 OR ((triple7 triple10) -> rule4) OR ((((triple8 triple6) -> rule7) triple10) -> rule4))] Erin is round.[(triple10 OR ((triple7 triple9) -> rule6) OR ((((triple8 triple6) -> rule7) triple9) -> rule6))] Erin is young.[(triple11 OR ((triple9) -> rule5) OR ((((triple7 triple10) -> rule4)) -> rule5) OR ((((((triple8 triple6) -> rule7) triple10) -> rule4)) -> rule5))] Gary is kind.[(triple12)] Gary is nice.[(triple13)] Gary is quiet.[(triple14 OR ((triple12 triple15) -> rule4))] Gary is round.[(triple15 OR ((triple12 triple14) -> rule6))] @1: Bob is kind.[(((triple1) -> rule1))] Bob is smart.[(((triple1) -> rule2) OR ((triple5) -> rule3) OR ((((triple3) -> rule5)) -> rule3) OR ((((((((triple1) -> rule1) triple4) -> rule4)) -> rule5)) -> rule3))] Erin is smart.[(((triple11) -> rule3) OR ((triple6) -> rule2) OR ((((triple7) -> rule8)) -> rule2) OR ((((triple9) -> rule5)) -> rule3) OR ((((((triple7 triple10) -> rule4)) -> rule5)) -> rule3) OR ((((((((triple8 triple6) -> rule7) triple10) -> rule4)) -> rule5)) -> rule3))] Gary is green.[(((triple12) -> rule8))] Gary is young.[(((triple14) -> rule5) OR ((((triple12 triple15) -> rule4)) -> rule5))] @2: Gary is smart.[(((((triple12) -> rule8)) -> rule2) OR ((((triple14) -> rule5)) -> rule3) OR ((((((triple12 triple15) -> rule4)) -> rule5)) -> rule3))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
((((triple1) -> (rule1 % int2)) triple4) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
triple4
((((triple1) -> (rule1 % int2)) triple3) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
triple5
((triple3) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((((((triple1) -> (rule1 % int3)) triple4) -> (rule4 % int2))) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
triple6
((triple7) -> (rule8 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple7
((triple8 triple6) -> (rule7 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
triple8
Erin is quiet.
("Erin" "is" "quiet" "+")
triple9
((triple7 triple10) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple8 triple6) -> (rule7 % int2)) triple10) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
triple10
((triple7 triple9) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((((triple8 triple6) -> (rule7 % int2)) triple9) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
triple11
((triple9) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((triple7 triple10) -> (rule4 % int2))) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((((triple8 triple6) -> (rule7 % int3)) triple10) -> (rule4 % int2))) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
triple12
Gary is nice.
("Gary" "is" "nice" "+")
triple13
Gary is quiet.
("Gary" "is" "quiet" "+")
triple14
((triple12 triple15) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
triple15
((triple12 triple14) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((triple1) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple5) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((((((((triple1) -> (rule1 % int4)) triple4) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
Erin is smart.
("Erin" "is" "smart" "+")
((triple11) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple6) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple7) -> (rule8 % int2))) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((triple9) -> (rule5 % int2))) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((((((triple7 triple10) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
((((((((triple8 triple6) -> (rule7 % int4)) triple10) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
Gary is green.
("Gary" "is" "green" "+")
((triple12) -> (rule8 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple14) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((((triple12 triple15) -> (rule4 % int2))) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((((triple12) -> (rule8 % int2))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((triple14) -> (rule5 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((((((triple12 triple15) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3