Bob is big. Bob is green. Bob is kind. Bob is nice. Bob is red. Bob is smart. Bob is young. Charlie is big. Charlie is green. Charlie is nice. Charlie is smart. Charlie is young. Fiona is big. Fiona is green. Fiona is kind. Fiona is red. All kind people are smart. Kind people are green. If Charlie is green then Charlie is red. Kind, red people are nice. Young, red people are nice. All nice, green people are young.
Bob is big.
("Bob" "is" "big" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is red.
("Fiona" "is" "red" "+")
All kind people are smart.
((("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
Kind people are green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
If Charlie is green then Charlie is red.
((("Charlie" "is" "green" "+")) -> ("Charlie" "is" "red" "+"))
Kind, red people are nice.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
Young, red people are nice.
((("someone" "is" "young" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
All nice, green people are young.
((("someone" "is" "nice" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
Bob is young.
True
1
proof
[(triple7 OR ((triple4 triple2) -> rule6) OR ((triple4 ((triple3) -> rule2)) -> rule6) OR ((((triple3 triple5) -> rule4) triple2) -> rule6) OR ((((triple3 triple5) -> rule4) ((triple3) -> rule2)) -> rule6))]
("Bob" "is" "young" "+")
triple7
((triple4 triple2) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((triple4 ((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((triple3 triple5) -> (rule4 % int2)) triple2) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((triple3 triple5) -> (rule4 % int3)) ((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Charlie is not nice.
False
1
inv-proof
[(triple10 OR ((triple12 ((triple9) -> rule3)) -> rule5))]
("Charlie" "is" "nice" "-")
triple10
((triple12 ((triple9) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Fiona is nice.
True
3
proof
[(((triple15 triple16) -> rule4))]
("Fiona" "is" "nice" "+")
((triple15 triple16) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Charlie is not red.
False
2
inv-proof
[(((triple9) -> rule3))]
("Charlie" "is" "red" "-")
((triple9) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Fiona is young.
True
5
proof
[(((((triple15 triple16) -> rule4) triple14) -> rule6) OR ((((triple15 triple16) -> rule4) ((triple15) -> rule2)) -> rule6))]
("Fiona" "is" "young" "+")
((((triple15 triple16) -> (rule4 % int2)) triple14) -> (rule6 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
((((triple15 triple16) -> (rule4 % int3)) ((triple15) -> (rule2 % int2))) -> (rule6 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is not young.
False
5
inv-proof
[(((((triple15 triple16) -> rule4) triple14) -> rule6) OR ((((triple15 triple16) -> rule4) ((triple15) -> rule2)) -> rule6))]
("Fiona" "is" "young" "-")
((((triple15 triple16) -> (rule4 % int2)) triple14) -> (rule6 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
((((triple15 triple16) -> (rule4 % int3)) ((triple15) -> (rule2 % int2))) -> (rule6 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
@0: Bob is big.[(triple1)] Bob is green.[(triple2 OR ((triple3) -> rule2))] Bob is kind.[(triple3)] Bob is nice.[(triple4 OR ((triple3 triple5) -> rule4) OR ((triple7 triple5) -> rule5))] Bob is red.[(triple5)] Bob is smart.[(triple6 OR ((triple3) -> rule1))] Bob is young.[(triple7 OR ((triple4 triple2) -> rule6) OR ((triple4 ((triple3) -> rule2)) -> rule6) OR ((((triple3 triple5) -> rule4) triple2) -> rule6) OR ((((triple3 triple5) -> rule4) ((triple3) -> rule2)) -> rule6))] Charlie is big.[(triple8)] Charlie is green.[(triple9)] Charlie is nice.[(triple10 OR ((triple12 ((triple9) -> rule3)) -> rule5))] Charlie is smart.[(triple11)] Charlie is young.[(triple12 OR ((triple10 triple9) -> rule6))] Fiona is big.[(triple13)] Fiona is green.[(triple14 OR ((triple15) -> rule2))] Fiona is kind.[(triple15)] Fiona is red.[(triple16)] @1: Charlie is red.[(((triple9) -> rule3))] Fiona is nice.[(((triple15 triple16) -> rule4))] Fiona is smart.[(((triple15) -> rule1))] @2: Fiona is young.[(((((triple15 triple16) -> rule4) triple14) -> rule6) OR ((((triple15 triple16) -> rule4) ((triple15) -> rule2)) -> rule6))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
((triple3) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
((triple3 triple5) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple7 triple5) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple5
Bob is smart.
("Bob" "is" "smart" "+")
triple6
((triple3) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
triple7
((triple4 triple2) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((triple4 ((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((triple3 triple5) -> (rule4 % int2)) triple2) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((triple3 triple5) -> (rule4 % int3)) ((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
triple8
Charlie is green.
("Charlie" "is" "green" "+")
triple9
Charlie is nice.
("Charlie" "is" "nice" "+")
triple10
((triple12 ((triple9) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple11
Charlie is young.
("Charlie" "is" "young" "+")
triple12
((triple10 triple9) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
triple13
Fiona is green.
("Fiona" "is" "green" "+")
triple14
((triple15) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
triple15
Fiona is red.
("Fiona" "is" "red" "+")
triple16
Charlie is red.
("Charlie" "is" "red" "+")
((triple9) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple15 triple16) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple15) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((((triple15 triple16) -> (rule4 % int2)) triple14) -> (rule6 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
((((triple15 triple16) -> (rule4 % int3)) ((triple15) -> (rule2 % int2))) -> (rule6 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3