Fiona is big. Fiona is kind. Fiona is nice. Fiona is red. Fiona is rough. Fiona is round. Fiona is young. Gary is kind. Gary is nice. Gary is red. Gary is round. Gary is young. If Gary is young and Gary is round then Gary is kind. Red, kind things are rough. Rough things are big.
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is young.
("Gary" "is" "young" "+")
If Gary is young and Gary is round then Gary is kind.
((("Gary" "is" "young" "+") ("Gary" "is" "round" "+")) -> ("Gary" "is" "kind" "+"))
Red, kind things are rough.
((("something" "is" "red" "+") ("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
Rough things are big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
Gary is kind.
True
1
proof
[(triple8 OR ((triple12 triple11) -> rule1))]
("Gary" "is" "kind" "+")
triple8
((triple12 triple11) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Fiona is not big.
False
1
inv-proof
[(triple1 OR ((triple5) -> rule3) OR ((((triple4 triple2) -> rule2)) -> rule3))]
("Fiona" "is" "big" "-")
triple1
((triple5) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((((triple4 triple2) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Gary is rough.
True
3
proof
[(((triple10 triple8) -> rule2) OR ((triple10 ((triple12 triple11) -> rule1)) -> rule2))]
("Gary" "is" "rough" "+")
((triple10 triple8) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((triple10 ((triple12 triple11) -> (rule1 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is not rough.
False
3
inv-proof
[(((triple10 triple8) -> rule2) OR ((triple10 ((triple12 triple11) -> rule1)) -> rule2))]
("Gary" "is" "rough" "-")
((triple10 triple8) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((triple10 ((triple12 triple11) -> (rule1 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is big.
True
4
proof
[(((((triple10 triple8) -> rule2)) -> rule3) OR ((((triple10 ((triple12 triple11) -> rule1)) -> rule2)) -> rule3))]
("Gary" "is" "big" "+")
((((triple10 triple8) -> (rule2 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((triple10 ((triple12 triple11) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is not big.
False
4
inv-proof
[(((((triple10 triple8) -> rule2)) -> rule3) OR ((((triple10 ((triple12 triple11) -> rule1)) -> rule2)) -> rule3))]
("Gary" "is" "big" "-")
((((triple10 triple8) -> (rule2 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((triple10 ((triple12 triple11) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
@0: Fiona is big.[(triple1 OR ((triple5) -> rule3) OR ((((triple4 triple2) -> rule2)) -> rule3))] Fiona is kind.[(triple2)] Fiona is nice.[(triple3)] Fiona is red.[(triple4)] Fiona is rough.[(triple5 OR ((triple4 triple2) -> rule2))] Fiona is round.[(triple6)] Fiona is young.[(triple7)] Gary is kind.[(triple8 OR ((triple12 triple11) -> rule1))] Gary is nice.[(triple9)] Gary is red.[(triple10)] Gary is round.[(triple11)] Gary is young.[(triple12)] @1: Gary is rough.[(((triple10 triple8) -> rule2) OR ((triple10 ((triple12 triple11) -> rule1)) -> rule2))] @2: Gary is big.[(((((triple10 triple8) -> rule2)) -> rule3) OR ((((triple10 ((triple12 triple11) -> rule1)) -> rule2)) -> rule3))]
Fiona is big.
("Fiona" "is" "big" "+")
triple1
((triple5) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((((triple4 triple2) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
triple2
Fiona is nice.
("Fiona" "is" "nice" "+")
triple3
Fiona is red.
("Fiona" "is" "red" "+")
triple4
Fiona is rough.
("Fiona" "is" "rough" "+")
triple5
((triple4 triple2) -> (rule2 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
triple6
Fiona is young.
("Fiona" "is" "young" "+")
triple7
Gary is kind.
("Gary" "is" "kind" "+")
triple8
((triple12 triple11) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
triple9
Gary is red.
("Gary" "is" "red" "+")
triple10
Gary is round.
("Gary" "is" "round" "+")
triple11
Gary is young.
("Gary" "is" "young" "+")
triple12
Gary is rough.
("Gary" "is" "rough" "+")
((triple10 triple8) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((triple10 ((triple12 triple11) -> (rule1 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
((((triple10 triple8) -> (rule2 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((triple10 ((triple12 triple11) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3