Dave is cold. Erin is big. Fiona is big. Harry is not blue. If something is round and big then it is young. All cold things are furry. If something is round and big then it is white. If something is big then it is round. If something is cold and not blue then it is round. White things are round. All white, big things are cold. If Harry is young then Harry is not round.
Dave is cold.
("Dave" "is" "cold" "+")
Erin is big.
("Erin" "is" "big" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Harry is not blue.
("Harry" "is" "blue" "-")
If something is round and big then it is young.
((("something" "is" "round" "+") ("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
All cold things are furry.
((("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
If something is round and big then it is white.
((("something" "is" "round" "+") ("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
If something is big then it is round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
If something is cold and not blue then it is round.
((("something" "is" "cold" "+") ("something" "is" "blue" "~")) -> ("something" "is" "round" "+"))
White things are round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
All white, big things are cold.
((("something" "is" "white" "+") ("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
If Harry is young then Harry is not round.
((("Harry" "is" "young" "+")) -> ("Harry" "is" "round" "-"))
Dave is cold.
True
1
proof
[(triple1)]
("Dave" "is" "cold" "+")
triple1
Harry is blue.
False
1
inv-proof
[(triple4)]
("Harry" "is" "blue" "+")
triple4
Dave is furry.
True
2
proof
[(((triple1) -> rule2))]
("Dave" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Erin is not round.
False
2
inv-proof
[(((triple2) -> rule4))]
("Erin" "is" "round" "-")
((triple2) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Fiona is young.
True
4
proof
[(((((triple3) -> rule4) triple3) -> rule1))]
("Fiona" "is" "young" "+")
((((triple3) -> (rule4 % int2)) triple3) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Erin is not white.
False
4
inv-proof
[(((((triple2) -> rule4) triple2) -> rule3))]
("Erin" "is" "white" "-")
((((triple2) -> (rule4 % int2)) triple2) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Fiona is cold.
True
6
proof
[(((((((triple3) -> rule4) triple3) -> rule3) triple3) -> rule7))]
("Fiona" "is" "cold" "+")
((((((triple3) -> (rule4 % int3)) triple3) -> (rule3 % int2)) triple3) -> (rule7 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is not cold.
False
6
inv-proof
[(((((((triple3) -> rule4) triple3) -> rule3) triple3) -> rule7))]
("Fiona" "is" "cold" "-")
((((((triple3) -> (rule4 % int3)) triple3) -> (rule3 % int2)) triple3) -> (rule7 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Dave is not young.
Unknown
inv-rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "young" "-")
Dave is white.
Unknown
rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "white" "+")
Harry is not white.
Unknown
inv-rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "white" "-")
Harry is young.
Unknown
rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "young" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Dave is cold.[(triple1)] Erin is big.[(triple2)] Fiona is big.[(triple3)] Harry is not blue.[(triple4)] @1: Dave is furry.[(((triple1) -> rule2))] Erin is round.[(((triple2) -> rule4))] Fiona is round.[(((triple3) -> rule4))] @2: Erin is white.[(((((triple2) -> rule4) triple2) -> rule3))] Erin is young.[(((((triple2) -> rule4) triple2) -> rule1))] Fiona is white.[(((((triple3) -> rule4) triple3) -> rule3))] Fiona is young.[(((((triple3) -> rule4) triple3) -> rule1))] @3: Erin is cold.[(((((((triple2) -> rule4) triple2) -> rule3) triple2) -> rule7))] Fiona is cold.[(((((((triple3) -> rule4) triple3) -> rule3) triple3) -> rule7))] @4: Erin is furry.[(((((((((triple2) -> rule4) triple2) -> rule3) triple2) -> rule7)) -> rule2))] Fiona is furry.[(((((((((triple3) -> rule4) triple3) -> rule3) triple3) -> rule7)) -> rule2))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Erin is big.
("Erin" "is" "big" "+")
triple2
Fiona is big.
("Fiona" "is" "big" "+")
triple3
Harry is not blue.
("Harry" "is" "blue" "-")
triple4
Dave is furry.
("Dave" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((triple2) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
((triple3) -> (rule4 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
((((triple3) -> (rule4 % int2)) triple3) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
((((triple3) -> (rule4 % int2)) triple3) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
((((((triple2) -> (rule4 % int3)) triple2) -> (rule3 % int2)) triple2) -> (rule7 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
((((((triple3) -> (rule4 % int3)) triple3) -> (rule3 % int2)) triple3) -> (rule7 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
((((((((triple2) -> (rule4 % int4)) triple2) -> (rule3 % int3)) triple2) -> (rule7 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
Fiona is furry.
("Fiona" "is" "furry" "+")
((((((((triple3) -> (rule4 % int4)) triple3) -> (rule3 % int3)) triple3) -> (rule7 % int2))) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
int4