Anne is blue. Anne is cold. Anne is green. Anne is kind. Anne is rough. Anne is round. Charlie is blue. Charlie is cold. Charlie is green. Charlie is kind. Charlie is rough. Charlie is round. If something is blue then it is cold. All cold, kind things are smart. If Charlie is rough and Charlie is round then Charlie is kind.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
If something is blue then it is cold.
((("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
All cold, kind things are smart.
((("something" "is" "cold" "+") ("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
If Charlie is rough and Charlie is round then Charlie is kind.
((("Charlie" "is" "rough" "+") ("Charlie" "is" "round" "+")) -> ("Charlie" "is" "kind" "+"))
Anne is blue.
True
1
proof
[(triple1)]
("Anne" "is" "blue" "+")
triple1
Charlie is not green.
False
1
inv-proof
[(triple9)]
("Charlie" "is" "green" "-")
triple9
Charlie is smart.
True
3
proof
[(((triple8 triple10) -> rule2) OR ((triple8 ((triple11 triple12) -> rule3)) -> rule2) OR ((((triple7) -> rule1) triple10) -> rule2) OR ((((triple7) -> rule1) ((triple11 triple12) -> rule3)) -> rule2))]
("Charlie" "is" "smart" "+")
((triple8 triple10) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((triple8 ((triple11 triple12) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple7) -> (rule1 % int2)) triple10) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((triple7) -> (rule1 % int3)) ((triple11 triple12) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is not smart.
False
3
inv-proof
[(((triple8 triple10) -> rule2) OR ((triple8 ((triple11 triple12) -> rule3)) -> rule2) OR ((((triple7) -> rule1) triple10) -> rule2) OR ((((triple7) -> rule1) ((triple11 triple12) -> rule3)) -> rule2))]
("Charlie" "is" "smart" "-")
((triple8 triple10) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((triple8 ((triple11 triple12) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple7) -> (rule1 % int2)) triple10) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((triple7) -> (rule1 % int3)) ((triple11 triple12) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
@0: Anne is blue.[(triple1)] Anne is cold.[(triple2 OR ((triple1) -> rule1))] Anne is green.[(triple3)] Anne is kind.[(triple4)] Anne is rough.[(triple5)] Anne is round.[(triple6)] Charlie is blue.[(triple7)] Charlie is cold.[(triple8 OR ((triple7) -> rule1))] Charlie is green.[(triple9)] Charlie is kind.[(triple10 OR ((triple11 triple12) -> rule3))] Charlie is rough.[(triple11)] Charlie is round.[(triple12)] @1: Anne is smart.[(((triple2 triple4) -> rule2) OR ((((triple1) -> rule1) triple4) -> rule2))] Charlie is smart.[(((triple8 triple10) -> rule2) OR ((triple8 ((triple11 triple12) -> rule3)) -> rule2) OR ((((triple7) -> rule1) triple10) -> rule2) OR ((((triple7) -> rule1) ((triple11 triple12) -> rule3)) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
((triple1) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
triple3
Anne is kind.
("Anne" "is" "kind" "+")
triple4
Anne is rough.
("Anne" "is" "rough" "+")
triple5
Anne is round.
("Anne" "is" "round" "+")
triple6
Charlie is blue.
("Charlie" "is" "blue" "+")
triple7
Charlie is cold.
("Charlie" "is" "cold" "+")
triple8
((triple7) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
triple9
Charlie is kind.
("Charlie" "is" "kind" "+")
triple10
((triple11 triple12) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple11
Charlie is round.
("Charlie" "is" "round" "+")
triple12
Anne is smart.
("Anne" "is" "smart" "+")
((triple2 triple4) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple1) -> (rule1 % int2)) triple4) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple8 triple10) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((triple8 ((triple11 triple12) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple7) -> (rule1 % int2)) triple10) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((triple7) -> (rule1 % int3)) ((triple11 triple12) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3