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