Charlie is cold. Charlie is kind. Charlie is nice. Charlie is quiet. Charlie is red. Charlie is rough. Charlie is round. Erin is cold. Erin is kind. Erin is nice. Erin is quiet. Erin is red. Erin is rough. Erin is round. If someone is nice then they are cold.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
If someone is nice then they are cold.
((("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
Erin is rough.
True
1
proof
[(triple13)]
("Erin" "is" "rough" "+")
triple13
Charlie is not cold.
False
1
inv-proof
[(triple1 OR ((triple3) -> rule1))]
("Charlie" "is" "cold" "-")
triple1
((triple3) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
@0: Charlie is cold.[(triple1 OR ((triple3) -> rule1))] Charlie is kind.[(triple2)] Charlie is nice.[(triple3)] Charlie is quiet.[(triple4)] Charlie is red.[(triple5)] Charlie is rough.[(triple6)] Charlie is round.[(triple7)] Erin is cold.[(triple8 OR ((triple10) -> rule1))] Erin is kind.[(triple9)] Erin is nice.[(triple10)] Erin is quiet.[(triple11)] Erin is red.[(triple12)] Erin is rough.[(triple13)] Erin is round.[(triple14)]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
((triple3) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
Charlie is red.
("Charlie" "is" "red" "+")
triple5
Charlie is rough.
("Charlie" "is" "rough" "+")
triple6
Charlie is round.
("Charlie" "is" "round" "+")
triple7
Erin is cold.
("Erin" "is" "cold" "+")
triple8
((triple10) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple9
Erin is nice.
("Erin" "is" "nice" "+")
triple10
Erin is quiet.
("Erin" "is" "quiet" "+")
triple11
Erin is red.
("Erin" "is" "red" "+")
triple12
Erin is rough.
("Erin" "is" "rough" "+")
triple13
Erin is round.
("Erin" "is" "round" "+")
triple14