Bob is green. Bob is kind. Bob is nice. Bob is rough. Charlie is green. Charlie is kind. Charlie is nice. All nice people are round. If someone is kind and rough then they are nice. All green, blue people are kind. All nice people are blue. If someone is round then they are green. Round people are cold.
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
All nice people are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
If someone is kind and rough then they are nice.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
All green, blue people are kind.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
All nice people are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
If someone is round then they are green.
((("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
Round people are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
Charlie is nice.
True
1
proof
[(triple7)]
("Charlie" "is" "nice" "+")
triple7
Charlie is not kind.
False
1
inv-proof
[(triple6 OR ((triple5 ((triple7) -> rule4)) -> rule3) OR ((((((triple7) -> rule1)) -> rule5) ((triple7) -> rule4)) -> rule3))]
("Charlie" "is" "kind" "-")
triple6
((triple5 ((triple7) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((((triple7) -> (rule1 % int4))) -> (rule5 % int3)) ((triple7) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
Bob is round.
True
2
proof
[(((triple3) -> rule1) OR ((((triple2 triple4) -> rule2)) -> rule1))]
("Bob" "is" "round" "+")
((triple3) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((((triple2 triple4) -> (rule2 % int2))) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is not blue.
False
2
inv-proof
[(((triple3) -> rule4) OR ((((triple2 triple4) -> rule2)) -> rule4))]
("Bob" "is" "blue" "-")
((triple3) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple2 triple4) -> (rule2 % int2))) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
@0: Bob is green.[(triple1 OR ((((triple3) -> rule1)) -> rule5) OR ((((((triple2 triple4) -> rule2)) -> rule1)) -> rule5))] Bob is kind.[(triple2 OR ((triple1 ((triple3) -> rule4)) -> rule3) OR ((((((triple3) -> rule1)) -> rule5) ((triple3) -> rule4)) -> rule3))] Bob is nice.[(triple3 OR ((triple2 triple4) -> rule2))] Bob is rough.[(triple4)] Charlie is green.[(triple5 OR ((((triple7) -> rule1)) -> rule5))] Charlie is kind.[(triple6 OR ((triple5 ((triple7) -> rule4)) -> rule3) OR ((((((triple7) -> rule1)) -> rule5) ((triple7) -> rule4)) -> rule3))] Charlie is nice.[(triple7)] @1: Bob is blue.[(((triple3) -> rule4) OR ((((triple2 triple4) -> rule2)) -> rule4))] Bob is round.[(((triple3) -> rule1) OR ((((triple2 triple4) -> rule2)) -> rule1))] Charlie is blue.[(((triple7) -> rule4))] Charlie is round.[(((triple7) -> rule1))] @2: Bob is cold.[(((((triple3) -> rule1)) -> rule6) OR ((((((triple2 triple4) -> rule2)) -> rule1)) -> rule6))] Charlie is cold.[(((((triple7) -> rule1)) -> rule6))]
Bob is green.
("Bob" "is" "green" "+")
triple1
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((((triple2 triple4) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
triple2
((triple1 ((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((((triple3) -> (rule1 % int4))) -> (rule5 % int3)) ((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Bob is nice.
("Bob" "is" "nice" "+")
triple3
((triple2 triple4) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
triple4
Charlie is green.
("Charlie" "is" "green" "+")
triple5
((((triple7) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple6
((triple5 ((triple7) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((((triple7) -> (rule1 % int4))) -> (rule5 % int3)) ((triple7) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
Charlie is nice.
("Charlie" "is" "nice" "+")
triple7
Bob is blue.
("Bob" "is" "blue" "+")
((triple3) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple2 triple4) -> (rule2 % int2))) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
((triple3) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((((triple2 triple4) -> (rule2 % int2))) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple7) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple7) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((((triple2 triple4) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple7) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2