Charlie is not big. Charlie is cold. Charlie is kind. Charlie is nice. Charlie is red. Charlie is rough. Charlie is round. Gary is big. Gary is cold. Gary is kind. Gary is nice. Gary is not red. Gary is rough. Gary is round. All big things are cold. All round things are cold. If something is nice then it is cold. Nice things are cold. If Charlie is kind then Charlie is cold. If something is cold then it is round. If something is cold then it is round. All big things are kind.
Charlie is not big.
("Charlie" "is" "big" "-")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is not red.
("Gary" "is" "red" "-")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
All big things are cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
All round things are cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
If something is nice then it is cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
Nice things are cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If Charlie is kind then Charlie is cold.
((("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "cold" "+"))
If something is cold then it is round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
If something is cold then it is round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
All big things are kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
Gary is not red.
True
1
proof
[(triple12)]
("Gary" "is" "red" "-")
triple12
Gary is not big.
False
1
inv-proof
[(triple8)]
("Gary" "is" "big" "-")
triple8
@0: Charlie is cold.[(triple2 OR ((triple3) -> rule5) OR ((triple4) -> rule3) OR ((triple4) -> rule4) OR ((triple7) -> rule2))] Charlie is kind.[(triple3)] Charlie is nice.[(triple4)] Charlie is not big.[(triple1)] Charlie is red.[(triple5)] Charlie is rough.[(triple6)] Charlie is round.[(triple7 OR ((triple2) -> rule6) OR ((triple2) -> rule7) OR ((((triple3) -> rule5)) -> rule6) OR ((((triple3) -> rule5)) -> rule7) OR ((((triple4) -> rule3)) -> rule6) OR ((((triple4) -> rule3)) -> rule7) OR ((((triple4) -> rule4)) -> rule6) OR ((((triple4) -> rule4)) -> rule7))] Gary is big.[(triple8)] Gary is cold.[(triple9 OR ((triple11) -> rule3) OR ((triple11) -> rule4) OR ((triple14) -> rule2) OR ((triple8) -> rule1))] Gary is kind.[(triple10 OR ((triple8) -> rule8))] Gary is nice.[(triple11)] Gary is not red.[(triple12)] Gary is rough.[(triple13)] Gary is round.[(triple14 OR ((triple9) -> rule6) OR ((triple9) -> rule7) OR ((((triple11) -> rule3)) -> rule6) OR ((((triple11) -> rule3)) -> rule7) OR ((((triple11) -> rule4)) -> rule6) OR ((((triple11) -> rule4)) -> rule7) OR ((((triple8) -> rule1)) -> rule6) OR ((((triple8) -> rule1)) -> rule7))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
((triple3) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((triple4) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((triple4) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((triple7) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Charlie is not big.
("Charlie" "is" "big" "-")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple5
Charlie is rough.
("Charlie" "is" "rough" "+")
triple6
Charlie is round.
("Charlie" "is" "round" "+")
triple7
((triple2) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((triple2) -> (rule7 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((triple3) -> (rule5 % int2))) -> (rule7 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((triple4) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((triple4) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((triple4) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((triple4) -> (rule4 % int2))) -> (rule7 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
triple8
Gary is cold.
("Gary" "is" "cold" "+")
triple9
((triple11) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((triple11) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((triple14) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((triple8) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple10
((triple8) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
triple11
Gary is not red.
("Gary" "is" "red" "-")
triple12
Gary is rough.
("Gary" "is" "rough" "+")
triple13
Gary is round.
("Gary" "is" "round" "+")
triple14
((triple9) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple9) -> (rule7 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((triple11) -> (rule3 % int2))) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((((triple11) -> (rule3 % int2))) -> (rule7 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((((triple11) -> (rule4 % int2))) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((((triple11) -> (rule4 % int2))) -> (rule7 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((((triple8) -> (rule1 % int2))) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((((triple8) -> (rule1 % int2))) -> (rule7 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2