Fiona is cold. Fiona is green. Fiona is kind. Fiona is rough. Fiona is smart. Fiona is young. Gary is blue. Gary is green. Gary is kind. Gary is rough. All smart things are cold. Cold things are blue. Rough things are young. If something is rough and blue then it is green. If something is cold then it is smart. Young things are smart.
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is rough.
("Gary" "is" "rough" "+")
All smart things are cold.
((("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
Cold things are blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
Rough things are young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If something is rough and blue then it is green.
((("something" "is" "rough" "+") ("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
If something is cold then it is smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
Young things are smart.
((("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
Fiona is cold.
True
1
proof
[(triple1 OR ((triple5) -> rule1) OR ((((triple6) -> rule6)) -> rule1) OR ((((((triple4) -> rule3)) -> rule6)) -> rule1))]
("Fiona" "is" "cold" "+")
triple1
((triple5) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((((triple6) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((((triple4) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Gary is not blue.
False
1
inv-proof
[(triple7 OR ((((((((triple10) -> rule3)) -> rule6)) -> rule1)) -> rule2))]
("Gary" "is" "blue" "-")
triple7
((((((((triple10) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is young.
("Gary" "is" "young" "+")
int4
Gary is young.
True
2
proof
[(((triple10) -> rule3))]
("Gary" "is" "young" "+")
((triple10) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not young.
False
2
inv-proof
[(((triple10) -> rule3))]
("Gary" "is" "young" "-")
((triple10) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
True
3
proof
[(((((triple10) -> rule3)) -> rule6))]
("Gary" "is" "smart" "+")
((((triple10) -> (rule3 % int2))) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is not smart.
False
3
inv-proof
[(((((triple10) -> rule3)) -> rule6))]
("Gary" "is" "smart" "-")
((((triple10) -> (rule3 % int2))) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is cold.
True
4
proof
[(((((((triple10) -> rule3)) -> rule6)) -> rule1))]
("Gary" "is" "cold" "+")
((((((triple10) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is not cold.
False
4
inv-proof
[(((((((triple10) -> rule3)) -> rule6)) -> rule1))]
("Gary" "is" "cold" "-")
((((((triple10) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
@0: Fiona is cold.[(triple1 OR ((triple5) -> rule1) OR ((((triple6) -> rule6)) -> rule1) OR ((((((triple4) -> rule3)) -> rule6)) -> rule1))] Fiona is green.[(triple2 OR ((triple4 ((triple1) -> rule2)) -> rule4) OR ((triple4 ((((triple5) -> rule1)) -> rule2)) -> rule4) OR ((triple4 ((((((triple6) -> rule6)) -> rule1)) -> rule2)) -> rule4) OR ((triple4 ((((((((triple4) -> rule3)) -> rule6)) -> rule1)) -> rule2)) -> rule4))] Fiona is kind.[(triple3)] Fiona is rough.[(triple4)] Fiona is smart.[(triple5 OR ((triple1) -> rule5) OR ((triple6) -> rule6) OR ((((triple4) -> rule3)) -> rule6))] Fiona is young.[(triple6 OR ((triple4) -> rule3))] Gary is blue.[(triple7 OR ((((((((triple10) -> rule3)) -> rule6)) -> rule1)) -> rule2))] Gary is green.[(triple8 OR ((triple10 triple7) -> rule4) OR ((triple10 ((((((((triple10) -> rule3)) -> rule6)) -> rule1)) -> rule2)) -> rule4))] Gary is kind.[(triple9)] Gary is rough.[(triple10)] @1: Fiona is blue.[(((triple1) -> rule2) OR ((((triple5) -> rule1)) -> rule2) OR ((((((triple6) -> rule6)) -> rule1)) -> rule2) OR ((((((((triple4) -> rule3)) -> rule6)) -> rule1)) -> rule2))] Gary is young.[(((triple10) -> rule3))] @2: Gary is smart.[(((((triple10) -> rule3)) -> rule6))] @3: Gary is cold.[(((((((triple10) -> rule3)) -> rule6)) -> rule1))]
Fiona is cold.
("Fiona" "is" "cold" "+")
triple1
((triple5) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((((triple6) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((((triple4) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
triple2
((triple4 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
((triple4 ((((triple5) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
((triple4 ((((((triple6) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
((triple4 ((((((((triple4) -> (rule3 % int5))) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
Fiona is young.
("Fiona" "is" "young" "+")
int5
Fiona is kind.
("Fiona" "is" "kind" "+")
triple3
Fiona is rough.
("Fiona" "is" "rough" "+")
triple4
Fiona is smart.
("Fiona" "is" "smart" "+")
triple5
((triple1) -> (rule5 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple6) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
triple6
((triple4) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
triple7
((((((((triple10) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is young.
("Gary" "is" "young" "+")
int4
Gary is green.
("Gary" "is" "green" "+")
triple8
((triple10 triple7) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((triple10 ((((((((triple10) -> (rule3 % int5))) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is young.
("Gary" "is" "young" "+")
int5
Gary is kind.
("Gary" "is" "kind" "+")
triple9
Gary is rough.
("Gary" "is" "rough" "+")
triple10
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple1) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((((((triple6) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
((((((((triple4) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is young.
("Fiona" "is" "young" "+")
int4
Gary is young.
("Gary" "is" "young" "+")
((triple10) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((((triple10) -> (rule3 % int2))) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((((((triple10) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3