Charlie is blue. Charlie is kind. Charlie is nice. Charlie is red. Charlie is smart. Gary is blue. Gary is cold. Gary is kind. Gary is nice. Gary is red. Gary is round. Gary is smart. If Charlie is nice then Charlie is red. If Charlie is cold then Charlie is blue. Blue things are round. If Gary is smart and Gary is cold then Gary is kind. Red, smart things are blue. If Charlie is nice then Charlie is kind.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If Charlie is nice then Charlie is red.
((("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "red" "+"))
If Charlie is cold then Charlie is blue.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "blue" "+"))
Blue things are round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
If Gary is smart and Gary is cold then Gary is kind.
((("Gary" "is" "smart" "+") ("Gary" "is" "cold" "+")) -> ("Gary" "is" "kind" "+"))
Red, smart things are blue.
((("something" "is" "red" "+") ("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
If Charlie is nice then Charlie is kind.
((("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "kind" "+"))
Charlie is red.
True
1
proof
[(triple4 OR ((triple3) -> rule1))]
("Charlie" "is" "red" "+")
triple4
((triple3) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Gary is not kind.
False
1
inv-proof
[(triple8 OR ((triple12 triple7) -> rule4))]
("Gary" "is" "kind" "-")
triple8
((triple12 triple7) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Charlie is round.
True
2
proof
[(((triple1) -> rule3) OR ((((triple4 triple5) -> rule5)) -> rule3) OR ((((((triple3) -> rule1) triple5) -> rule5)) -> rule3))]
("Charlie" "is" "round" "+")
((triple1) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((triple4 triple5) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((((triple3) -> (rule1 % int3)) triple5) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is not round.
False
2
inv-proof
[(((triple1) -> rule3) OR ((((triple4 triple5) -> rule5)) -> rule3) OR ((((((triple3) -> rule1) triple5) -> rule5)) -> rule3))]
("Charlie" "is" "round" "-")
((triple1) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((triple4 triple5) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((((triple3) -> (rule1 % int3)) triple5) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
@0: Charlie is blue.[(triple1 OR ((triple4 triple5) -> rule5) OR ((((triple3) -> rule1) triple5) -> rule5))] Charlie is kind.[(triple2 OR ((triple3) -> rule6))] Charlie is nice.[(triple3)] Charlie is red.[(triple4 OR ((triple3) -> rule1))] Charlie is smart.[(triple5)] Gary is blue.[(triple6 OR ((triple10 triple12) -> rule5))] Gary is cold.[(triple7)] Gary is kind.[(triple8 OR ((triple12 triple7) -> rule4))] Gary is nice.[(triple9)] Gary is red.[(triple10)] Gary is round.[(triple11 OR ((triple6) -> rule3) OR ((((triple10 triple12) -> rule5)) -> rule3))] Gary is smart.[(triple12)] @1: Charlie is round.[(((triple1) -> rule3) OR ((((triple4 triple5) -> rule5)) -> rule3) OR ((((((triple3) -> rule1) triple5) -> rule5)) -> rule3))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
((triple4 triple5) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((((triple3) -> (rule1 % int2)) triple5) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
((triple3) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple4
((triple3) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
Gary is blue.
("Gary" "is" "blue" "+")
triple6
((triple10 triple12) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
triple7
Gary is kind.
("Gary" "is" "kind" "+")
triple8
((triple12 triple7) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
triple9
Gary is red.
("Gary" "is" "red" "+")
triple10
Gary is round.
("Gary" "is" "round" "+")
triple11
((triple6) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((triple10 triple12) -> (rule5 % int2))) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
triple12
Charlie is round.
("Charlie" "is" "round" "+")
((triple1) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((triple4 triple5) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((((triple3) -> (rule1 % int3)) triple5) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3