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