Charlie is big. Charlie is blue. Charlie is red. Charlie is white. Charlie is not young. Fiona is big. Fiona is blue. Fiona is not red. Fiona is rough. Fiona is smart. Fiona is white. Fiona is young. If Charlie is big and Charlie is red then Charlie is blue. Big, blue people are rough. If someone is rough then they are smart.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is not young.
("Charlie" "is" "young" "-")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is not red.
("Fiona" "is" "red" "-")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Fiona is young.
("Fiona" "is" "young" "+")
If Charlie is big and Charlie is red then Charlie is blue.
((("Charlie" "is" "big" "+") ("Charlie" "is" "red" "+")) -> ("Charlie" "is" "blue" "+"))
Big, blue people are rough.
((("someone" "is" "big" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
If someone is rough then they are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
Fiona is young.
True
1
proof
[(triple12)]
("Fiona" "is" "young" "+")
triple12
Fiona is not white.
False
1
inv-proof
[(triple11)]
("Fiona" "is" "white" "-")
triple11
Charlie is rough.
True
3
proof
[(((triple1 triple2) -> rule2) OR ((triple1 ((triple1 triple3) -> rule1)) -> rule2))]
("Charlie" "is" "rough" "+")
((triple1 triple2) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple1 ((triple1 triple3) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is not rough.
False
3
inv-proof
[(((triple1 triple2) -> rule2) OR ((triple1 ((triple1 triple3) -> rule1)) -> rule2))]
("Charlie" "is" "rough" "-")
((triple1 triple2) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple1 ((triple1 triple3) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is smart.
True
4
proof
[(((((triple1 triple2) -> rule2)) -> rule3) OR ((((triple1 ((triple1 triple3) -> rule1)) -> rule2)) -> rule3))]
("Charlie" "is" "smart" "+")
((((triple1 triple2) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((triple1 ((triple1 triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is not smart.
False
4
inv-proof
[(((((triple1 triple2) -> rule2)) -> rule3) OR ((((triple1 ((triple1 triple3) -> rule1)) -> rule2)) -> rule3))]
("Charlie" "is" "smart" "-")
((((triple1 triple2) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((triple1 ((triple1 triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
@0: Charlie is big.[(triple1)] Charlie is blue.[(triple2 OR ((triple1 triple3) -> rule1))] Charlie is not young.[(triple5)] Charlie is red.[(triple3)] Charlie is white.[(triple4)] Fiona is big.[(triple6)] Fiona is blue.[(triple7)] Fiona is not red.[(triple8)] Fiona is rough.[(triple9 OR ((triple6 triple7) -> rule2))] Fiona is smart.[(triple10 OR ((triple9) -> rule3) OR ((((triple6 triple7) -> rule2)) -> rule3))] Fiona is white.[(triple11)] Fiona is young.[(triple12)] @1: Charlie is rough.[(((triple1 triple2) -> rule2) OR ((triple1 ((triple1 triple3) -> rule1)) -> rule2))] @2: Charlie is smart.[(((((triple1 triple2) -> rule2)) -> rule3) OR ((((triple1 ((triple1 triple3) -> rule1)) -> rule2)) -> rule3))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
((triple1 triple3) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is not young.
("Charlie" "is" "young" "-")
triple5
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Charlie is white.
("Charlie" "is" "white" "+")
triple4
Fiona is big.
("Fiona" "is" "big" "+")
triple6
Fiona is blue.
("Fiona" "is" "blue" "+")
triple7
Fiona is not red.
("Fiona" "is" "red" "-")
triple8
Fiona is rough.
("Fiona" "is" "rough" "+")
triple9
((triple6 triple7) -> (rule2 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
triple10
((triple9) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((((triple6 triple7) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
triple11
Fiona is young.
("Fiona" "is" "young" "+")
triple12
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple1 triple2) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple1 ((triple1 triple3) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple1 triple2) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((triple1 ((triple1 triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3