Dave is cold. Dave is green. Dave is nice. Dave is quiet. Dave is red. Dave is smart. Dave is young. Erin is cold. Erin is smart. Erin is young. Gary is cold. Gary is green. Gary is nice. Gary is quiet. Gary is smart. Gary is young. Green things are nice. Young things are red. Red things are green.
Dave is cold.
("Dave" "is" "cold" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
Green things are nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
Young things are red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
Red things are green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
Gary is young.
True
1
proof
[(triple16)]
("Gary" "is" "young" "+")
triple16
Gary is not quiet.
False
1
inv-proof
[(triple14)]
("Gary" "is" "quiet" "-")
triple14
Erin is red.
True
2
proof
[(((triple10) -> rule2))]
("Erin" "is" "red" "+")
((triple10) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is not red.
False
2
inv-proof
[(((triple10) -> rule2))]
("Erin" "is" "red" "-")
((triple10) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
@0: Dave is cold.[(triple1)] Dave is green.[(triple2 OR ((triple5) -> rule3) OR ((((triple7) -> rule2)) -> rule3))] Dave is nice.[(triple3 OR ((triple2) -> rule1) OR ((((triple5) -> rule3)) -> rule1) OR ((((((triple7) -> rule2)) -> rule3)) -> rule1))] Dave is quiet.[(triple4)] Dave is red.[(triple5 OR ((triple7) -> rule2))] Dave is smart.[(triple6)] Dave is young.[(triple7)] Erin is cold.[(triple8)] Erin is smart.[(triple9)] Erin is young.[(triple10)] Gary is cold.[(triple11)] Gary is green.[(triple12 OR ((((triple16) -> rule2)) -> rule3))] Gary is nice.[(triple13 OR ((triple12) -> rule1) OR ((((((triple16) -> rule2)) -> rule3)) -> rule1))] Gary is quiet.[(triple14)] Gary is smart.[(triple15)] Gary is young.[(triple16)] @1: Erin is red.[(((triple10) -> rule2))] Gary is red.[(((triple16) -> rule2))] @2: Erin is green.[(((((triple10) -> rule2)) -> rule3))] @3: Erin is nice.[(((((((triple10) -> rule2)) -> rule3)) -> rule1))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
((triple5) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
((triple2) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((((((triple7) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
Dave is red.
("Dave" "is" "red" "+")
triple5
((triple7) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
Erin is cold.
("Erin" "is" "cold" "+")
triple8
Erin is smart.
("Erin" "is" "smart" "+")
triple9
Erin is young.
("Erin" "is" "young" "+")
triple10
Gary is cold.
("Gary" "is" "cold" "+")
triple11
Gary is green.
("Gary" "is" "green" "+")
triple12
((((triple16) -> (rule2 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
triple13
((triple12) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((((triple16) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
triple14
Gary is smart.
("Gary" "is" "smart" "+")
triple15
Gary is young.
("Gary" "is" "young" "+")
triple16
Erin is red.
("Erin" "is" "red" "+")
((triple10) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple16) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((((triple10) -> (rule2 % int2))) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
((((((triple10) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3