Anne is big. Anne is kind. Anne is quiet. Anne is rough. Bob is big. Bob is kind. Bob is quiet. Bob is round. Bob is young. Dave is big. Dave is quiet. Dave is round. Fiona is big. Fiona is kind. Fiona is rough. If something is big then it is young. If something is cold then it is kind. If something is quiet and cold then it is kind. If something is cold then it is round. If something is young and round then it is rough. If something is young then it is big. If Fiona is round then Fiona is big. If something is rough then it is cold.
Anne is big.
("Anne" "is" "big" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
If something is big then it is young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If something is cold then it is kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
If something is quiet and cold then it is kind.
((("something" "is" "quiet" "+") ("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
If something is cold then it is round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
If something is young and round then it is rough.
((("something" "is" "young" "+") ("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
If something is young then it is big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
If Fiona is round then Fiona is big.
((("Fiona" "is" "round" "+")) -> ("Fiona" "is" "big" "+"))
If something is rough then it is cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
Dave is big.
True
1
proof
[(triple10)]
("Dave" "is" "big" "+")
triple10
Bob is not young.
False
1
inv-proof
[(triple9 OR ((triple5) -> rule1))]
("Bob" "is" "young" "-")
triple9
((triple5) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Anne is cold.
True
2
proof
[(((triple4) -> rule8))]
("Anne" "is" "cold" "+")
((triple4) -> (rule8 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Fiona is not cold.
False
2
inv-proof
[(((triple15) -> rule8))]
("Fiona" "is" "cold" "-")
((triple15) -> (rule8 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is round.
True
3
proof
[(((((triple15) -> rule8)) -> rule4))]
("Fiona" "is" "round" "+")
((((triple15) -> (rule8 % int2))) -> (rule4 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Dave is not rough.
False
4
inv-proof
[(((((triple10) -> rule1) triple12) -> rule5))]
("Dave" "is" "rough" "-")
((((triple10) -> (rule1 % int2)) triple12) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is cold.
True
5
proof
[(((((((triple10) -> rule1) triple12) -> rule5)) -> rule8))]
("Dave" "is" "cold" "+")
((((((triple10) -> (rule1 % int3)) triple12) -> (rule5 % int2))) -> (rule8 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is not cold.
False
5
inv-proof
[(((((((triple10) -> rule1) triple12) -> rule5)) -> rule8))]
("Dave" "is" "cold" "-")
((((((triple10) -> (rule1 % int3)) triple12) -> (rule5 % int2))) -> (rule8 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
@0: Anne is big.[(triple1)] Anne is kind.[(triple2 OR ((((triple4) -> rule8)) -> rule2) OR ((triple3 ((triple4) -> rule8)) -> rule3))] Anne is quiet.[(triple3)] Anne is rough.[(triple4)] Bob is big.[(triple5 OR ((triple9) -> rule6))] Bob is kind.[(triple6 OR ((((((triple9 triple8) -> rule5)) -> rule8)) -> rule2) OR ((triple7 ((((triple9 triple8) -> rule5)) -> rule8)) -> rule3) OR ((((((((triple5) -> rule1) triple8) -> rule5)) -> rule8)) -> rule2) OR ((triple7 ((((((triple5) -> rule1) triple8) -> rule5)) -> rule8)) -> rule3))] Bob is quiet.[(triple7)] Bob is round.[(triple8)] Bob is young.[(triple9 OR ((triple5) -> rule1))] Dave is big.[(triple10)] Dave is quiet.[(triple11)] Dave is round.[(triple12)] Fiona is big.[(triple13 OR ((((((triple15) -> rule8)) -> rule4)) -> rule7))] Fiona is kind.[(triple14 OR ((((triple15) -> rule8)) -> rule2))] Fiona is rough.[(triple15)] @1: Anne is cold.[(((triple4) -> rule8))] Anne is young.[(((triple1) -> rule1))] Bob is rough.[(((triple9 triple8) -> rule5) OR ((((triple5) -> rule1) triple8) -> rule5))] Dave is young.[(((triple10) -> rule1))] Fiona is cold.[(((triple15) -> rule8))] Fiona is young.[(((triple13) -> rule1) OR ((((((((triple15) -> rule8)) -> rule4)) -> rule7)) -> rule1))] @2: Anne is round.[(((((triple4) -> rule8)) -> rule4))] Bob is cold.[(((((triple9 triple8) -> rule5)) -> rule8) OR ((((((triple5) -> rule1) triple8) -> rule5)) -> rule8))] Dave is rough.[(((((triple10) -> rule1) triple12) -> rule5))] Fiona is round.[(((((triple15) -> rule8)) -> rule4))] @3: Dave is cold.[(((((((triple10) -> rule1) triple12) -> rule5)) -> rule8))] @4: Dave is kind.[(((((((((triple10) -> rule1) triple12) -> rule5)) -> rule8)) -> rule2) OR ((triple11 ((((((triple10) -> rule1) triple12) -> rule5)) -> rule8)) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
((((triple4) -> (rule8 % int2))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((triple3 ((triple4) -> (rule8 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Bob is big.
("Bob" "is" "big" "+")
triple5
((triple9) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
triple6
((((((triple9 triple8) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
((triple7 ((((triple9 triple8) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
((((((((triple5) -> (rule1 % int4)) triple8) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
((triple7 ((((((triple5) -> (rule1 % int4)) triple8) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple7
Bob is round.
("Bob" "is" "round" "+")
triple8
Bob is young.
("Bob" "is" "young" "+")
triple9
((triple5) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
triple10
Dave is quiet.
("Dave" "is" "quiet" "+")
triple11
Dave is round.
("Dave" "is" "round" "+")
triple12
Fiona is big.
("Fiona" "is" "big" "+")
triple13
((((((triple15) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
triple14
((((triple15) -> (rule8 % int2))) -> (rule2 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
triple15
Anne is cold.
("Anne" "is" "cold" "+")
((triple4) -> (rule8 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((triple9 triple8) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple5) -> (rule1 % int2)) triple8) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
((triple10) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple15) -> (rule8 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((triple13) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((((((((triple15) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
int4
Anne is round.
("Anne" "is" "round" "+")
((((triple4) -> (rule8 % int2))) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
((((triple9 triple8) -> (rule5 % int2))) -> (rule8 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((((triple5) -> (rule1 % int3)) triple8) -> (rule5 % int2))) -> (rule8 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
((((triple10) -> (rule1 % int2)) triple12) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
((((triple15) -> (rule8 % int2))) -> (rule4 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
((((((triple10) -> (rule1 % int3)) triple12) -> (rule5 % int2))) -> (rule8 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
((((((((triple10) -> (rule1 % int4)) triple12) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
((triple11 ((((((triple10) -> (rule1 % int4)) triple12) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4