Charlie is green. Charlie is kind. Charlie is nice. Charlie is quiet. Charlie is red. Charlie is smart. Charlie is young. Fiona is green. Fiona is kind. Fiona is nice. Fiona is quiet. Fiona is red. Fiona is smart. Fiona is young. Smart, red things are nice. Smart things are quiet.
Charlie is green.
("Charlie" "is" "green" "+")
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 smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Smart, red things are nice.
((("something" "is" "smart" "+") ("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
Smart things are quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
Charlie is red.
True
1
proof
[(triple5)]
("Charlie" "is" "red" "+")
triple5
Fiona is not quiet.
False
1
inv-proof
[(triple11 OR ((triple13) -> rule2))]
("Fiona" "is" "quiet" "-")
triple11
((triple13) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
@0: Charlie is green.[(triple1)] Charlie is kind.[(triple2)] Charlie is nice.[(triple3 OR ((triple6 triple5) -> rule1))] Charlie is quiet.[(triple4 OR ((triple6) -> rule2))] Charlie is red.[(triple5)] Charlie is smart.[(triple6)] Charlie is young.[(triple7)] Fiona is green.[(triple8)] Fiona is kind.[(triple9)] Fiona is nice.[(triple10 OR ((triple13 triple12) -> rule1))] Fiona is quiet.[(triple11 OR ((triple13) -> rule2))] Fiona is red.[(triple12)] Fiona is smart.[(triple13)] Fiona is young.[(triple14)]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
((triple6 triple5) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
((triple6) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple5
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
Charlie is young.
("Charlie" "is" "young" "+")
triple7
Fiona is green.
("Fiona" "is" "green" "+")
triple8
Fiona is kind.
("Fiona" "is" "kind" "+")
triple9
Fiona is nice.
("Fiona" "is" "nice" "+")
triple10
((triple13 triple12) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple11
((triple13) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
triple12
Fiona is smart.
("Fiona" "is" "smart" "+")
triple13
Fiona is young.
("Fiona" "is" "young" "+")
triple14