Bob is big. Bob is blue. Bob is kind. Bob is red. Bob is rough. Bob is not smart. Bob is not young. Dave is red. Dave is rough. Dave is smart. Dave is young. Fiona is big. Fiona is kind. Fiona is red. Fiona is rough. Fiona is smart. All blue, young people are big. Smart people are kind. All kind, smart people are blue.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is not smart.
("Bob" "is" "smart" "-")
Bob is not young.
("Bob" "is" "young" "-")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
All blue, young people are big.
((("someone" "is" "blue" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
Smart people are kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
All kind, smart people are blue.
((("someone" "is" "kind" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
Fiona is red.
True
1
proof
[(triple14)]
("Fiona" "is" "red" "+")
triple14
Dave is not rough.
False
1
inv-proof
[(triple9)]
("Dave" "is" "rough" "-")
triple9
Fiona is blue.
True
3
proof
[(((triple13 triple16) -> rule3) OR ((((triple16) -> rule2) triple16) -> rule3))]
("Fiona" "is" "blue" "+")
((triple13 triple16) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((((triple16) -> (rule2 % int2)) triple16) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Dave is not kind.
False
2
inv-proof
[(((triple10) -> rule2))]
("Dave" "is" "kind" "-")
((triple10) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is blue.
True
4
proof
[(((((triple10) -> rule2) triple10) -> rule3))]
("Dave" "is" "blue" "+")
((((triple10) -> (rule2 % int2)) triple10) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is not blue.
False
4
inv-proof
[(((((triple10) -> rule2) triple10) -> rule3))]
("Dave" "is" "blue" "-")
((((triple10) -> (rule2 % int2)) triple10) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is big.
True
6
proof
[(((((((triple10) -> rule2) triple10) -> rule3) triple11) -> rule1))]
("Dave" "is" "big" "+")
((((((triple10) -> (rule2 % int3)) triple10) -> (rule3 % int2)) triple11) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is not big.
False
6
inv-proof
[(((((((triple10) -> rule2) triple10) -> rule3) triple11) -> rule1))]
("Dave" "is" "big" "-")
((((((triple10) -> (rule2 % int3)) triple10) -> (rule3 % int2)) triple11) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
@0: Bob is big.[(triple1)] Bob is blue.[(triple2)] Bob is kind.[(triple3)] Bob is not smart.[(triple6)] Bob is not young.[(triple7)] Bob is red.[(triple4)] Bob is rough.[(triple5)] Dave is red.[(triple8)] Dave is rough.[(triple9)] Dave is smart.[(triple10)] Dave is young.[(triple11)] Fiona is big.[(triple12)] Fiona is kind.[(triple13 OR ((triple16) -> rule2))] Fiona is red.[(triple14)] Fiona is rough.[(triple15)] Fiona is smart.[(triple16)] @1: Dave is kind.[(((triple10) -> rule2))] Fiona is blue.[(((triple13 triple16) -> rule3) OR ((((triple16) -> rule2) triple16) -> rule3))] @2: Dave is blue.[(((((triple10) -> rule2) triple10) -> rule3))] @3: Dave is big.[(((((((triple10) -> rule2) triple10) -> rule3) triple11) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is not smart.
("Bob" "is" "smart" "-")
triple6
Bob is not young.
("Bob" "is" "young" "-")
triple7
Bob is red.
("Bob" "is" "red" "+")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
triple5
Dave is red.
("Dave" "is" "red" "+")
triple8
Dave is rough.
("Dave" "is" "rough" "+")
triple9
Dave is smart.
("Dave" "is" "smart" "+")
triple10
Dave is young.
("Dave" "is" "young" "+")
triple11
Fiona is big.
("Fiona" "is" "big" "+")
triple12
Fiona is kind.
("Fiona" "is" "kind" "+")
triple13
((triple16) -> (rule2 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
triple14
Fiona is rough.
("Fiona" "is" "rough" "+")
triple15
Fiona is smart.
("Fiona" "is" "smart" "+")
triple16
Dave is kind.
("Dave" "is" "kind" "+")
((triple10) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple13 triple16) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((((triple16) -> (rule2 % int2)) triple16) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
((((triple10) -> (rule2 % int2)) triple10) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((((((triple10) -> (rule2 % int3)) triple10) -> (rule3 % int2)) triple11) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3