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