Bob is big. Bob is blue. Bob is cold. Bob is kind. Bob is nice. Fiona is big. Fiona is cold. Fiona is kind. Fiona is young. Gary is big. Gary is blue. Gary is cold. Gary is kind. Gary is nice. Gary is smart. Gary is young. All cold things are big. Cold, nice things are young. If Bob is young and Bob is big then Bob is kind. All smart things are nice. If Bob is cold and Bob is nice then Bob is smart. If something is kind then it is smart.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
All cold things are big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
Cold, nice things are young.
((("something" "is" "cold" "+") ("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
If Bob is young and Bob is big then Bob is kind.
((("Bob" "is" "young" "+") ("Bob" "is" "big" "+")) -> ("Bob" "is" "kind" "+"))
All smart things are nice.
((("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
If Bob is cold and Bob is nice then Bob is smart.
((("Bob" "is" "cold" "+") ("Bob" "is" "nice" "+")) -> ("Bob" "is" "smart" "+"))
If something is kind then it is smart.
((("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
Gary is cold.
True
1
proof
[(triple12)]
("Gary" "is" "cold" "+")
triple12
Bob is not blue.
False
1
inv-proof
[(triple2)]
("Bob" "is" "blue" "-")
triple2
Bob is smart.
True
2
proof
[(((triple4) -> rule6) OR ((triple3 triple5) -> rule5) OR ((((((triple3 triple5) -> rule2) triple1) -> rule3)) -> rule6) OR ((((((triple3 triple5) -> rule2) ((triple3) -> rule1)) -> rule3)) -> rule6))]
("Bob" "is" "smart" "+")
((triple4) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple3 triple5) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((((triple3 triple5) -> (rule2 % int3)) triple1) -> (rule3 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
((((((triple3 triple5) -> (rule2 % int4)) ((triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is not young.
False
3
inv-proof
[(((triple3 triple5) -> rule2) OR ((triple3 ((((triple4) -> rule6)) -> rule4)) -> rule2))]
("Bob" "is" "young" "-")
((triple3 triple5) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((triple3 ((((triple4) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Fiona is nice.
True
3
proof
[(((((triple8) -> rule6)) -> rule4))]
("Fiona" "is" "nice" "+")
((((triple8) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is not nice.
False
3
inv-proof
[(((((triple8) -> rule6)) -> rule4))]
("Fiona" "is" "nice" "-")
((((triple8) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
@0: Bob is big.[(triple1 OR ((triple3) -> rule1))] Bob is blue.[(triple2)] Bob is cold.[(triple3)] Bob is kind.[(triple4 OR ((((triple3 triple5) -> rule2) triple1) -> rule3) OR ((((triple3 triple5) -> rule2) ((triple3) -> rule1)) -> rule3))] Bob is nice.[(triple5 OR ((((triple4) -> rule6)) -> rule4))] Fiona is big.[(triple6 OR ((triple7) -> rule1))] Fiona is cold.[(triple7)] Fiona is kind.[(triple8)] Fiona is young.[(triple9 OR ((triple7 ((((triple8) -> rule6)) -> rule4)) -> rule2))] Gary is big.[(triple10 OR ((triple12) -> rule1))] Gary is blue.[(triple11)] Gary is cold.[(triple12)] Gary is kind.[(triple13)] Gary is nice.[(triple14 OR ((triple15) -> rule4) OR ((((triple13) -> rule6)) -> rule4))] Gary is smart.[(triple15 OR ((triple13) -> rule6))] Gary is young.[(triple16 OR ((triple12 triple14) -> rule2) OR ((triple12 ((triple15) -> rule4)) -> rule2) OR ((triple12 ((((triple13) -> rule6)) -> rule4)) -> rule2))] @1: Bob is smart.[(((triple4) -> rule6) OR ((triple3 triple5) -> rule5) OR ((((((triple3 triple5) -> rule2) triple1) -> rule3)) -> rule6) OR ((((((triple3 triple5) -> rule2) ((triple3) -> rule1)) -> rule3)) -> rule6))] Bob is young.[(((triple3 triple5) -> rule2) OR ((triple3 ((((triple4) -> rule6)) -> rule4)) -> rule2))] Fiona is smart.[(((triple8) -> rule6))] @2: Fiona is nice.[(((((triple8) -> rule6)) -> rule4))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple3) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is cold.
("Bob" "is" "cold" "+")
triple3
Bob is kind.
("Bob" "is" "kind" "+")
triple4
((((triple3 triple5) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((((triple3 triple5) -> (rule2 % int3)) ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
triple5
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
triple6
((triple7) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple7
Fiona is kind.
("Fiona" "is" "kind" "+")
triple8
Fiona is young.
("Fiona" "is" "young" "+")
triple9
((triple7 ((((triple8) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
triple10
((triple12) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
triple11
Gary is cold.
("Gary" "is" "cold" "+")
triple12
Gary is kind.
("Gary" "is" "kind" "+")
triple13
Gary is nice.
("Gary" "is" "nice" "+")
triple14
((triple15) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((triple13) -> (rule6 % int2))) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
triple15
((triple13) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
triple16
((triple12 triple14) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((triple12 ((triple15) -> (rule4 % int2))) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((triple12 ((((triple13) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
((triple4) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple3 triple5) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((((triple3 triple5) -> (rule2 % int3)) triple1) -> (rule3 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
((((((triple3 triple5) -> (rule2 % int4)) ((triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is young.
("Bob" "is" "young" "+")
((triple3 triple5) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((triple3 ((((triple4) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple8) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((((triple8) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2